# Theory DFS

(* Title: Presburger-Automata/DFS.thy Author: Toshiaki Nishihara and Yasuhiko Minamide Author: Stefan Berghofer and Alex Krauss, TU Muenchen, 2008-2009 *) section ‹Depth First Search› theory DFS imports Main begin definition "succsr succs = {(x, y). y ∈ set (succs x)}" partial_function (tailrec) gen_dfs where "gen_dfs succs ins memb S wl = (case wl of [] ⇒ S | x # xs ⇒ if memb x S then gen_dfs succs ins memb S xs else gen_dfs succs ins memb (ins x S) (succs x @ xs))" lemma gen_dfs_simps[simp]: "gen_dfs succs ins memb S [] = S" "gen_dfs succs ins memb S (x # xs) = (if memb x S then gen_dfs succs ins memb S xs else gen_dfs succs ins memb (ins x S) (succs x @ xs))" by (simp_all add: gen_dfs.simps) locale DFS = fixes succs :: "'a ⇒ 'a list" and is_node :: "'a ⇒ bool" and invariant :: "'b ⇒ bool" and ins :: "'a ⇒ 'b ⇒ 'b" and memb :: "'a ⇒ 'b ⇒ bool" and empt :: 'b assumes ins_eq: "⋀x y S. is_node x ⟹ is_node y ⟹ invariant S ⟹ ¬ memb y S ⟹ memb x (ins y S) = ((x = y) ∨ memb x S)" and empt: "⋀x. is_node x ⟹ ¬ memb x empt" and succs_is_node: "⋀x. is_node x ⟹ list_all is_node (succs x)" and empt_invariant: "invariant empt" and ins_invariant: "⋀x S. is_node x ⟹ invariant S ⟹ ¬ memb x S ⟹ invariant (ins x S)" and graph_finite: "finite {x. is_node x}" begin definition rel where "rel = inv_image finite_psubset (λS. {n. is_node n ∧ ¬ memb n S})" abbreviation "dfs ≡ gen_dfs succs ins memb" lemma dfs_induct [consumes 2, case_names base step]: assumes S: "invariant S" and xs: "list_all is_node xs" and I1: "⋀S. invariant S ⟹ P S []" and I2: "⋀S x xs. invariant S ⟹ is_node x ⟹ list_all is_node xs ⟹ (memb x S ⟹ P S xs) ⟹ (¬ memb x S ⟹ P (ins x S) (succs x @ xs)) ⟹ P S (x # xs)" shows "P S xs" using I1 I2 S xs apply induction_schema apply atomize_elim apply (case_tac xs, simp+) apply atomize_elim apply (rule conjI) apply (rule ins_invariant, assumption+) apply (rule succs_is_node, assumption) apply (relation "rel <*lex*> measure length") apply (simp add: wf_lex_prod rel_def) apply simp apply simp apply (rule disjI1) apply (simp add: rel_def finite_psubset_def) apply (rule conjI) apply (auto simp add: ins_eq graph_finite cong: conj_cong) done definition "succss xs = (⋃x∈xs. set (succs x))" definition "set_of S = {x. is_node x ∧ memb x S}" definition "reachable xs = {(x, y). y ∈ set (succs x)}⇧^{*}`` xs" lemma visit_subset_dfs: "invariant S ⟹ list_all is_node xs ⟹ is_node y ⟹ memb y S ⟹ memb y (dfs S xs)" by (induct S xs rule: dfs_induct) (simp_all add: ins_eq) lemma next_subset_dfs: "invariant S ⟹ list_all is_node xs ⟹ x ∈ set xs ⟹ memb x (dfs S xs)" proof (induct S xs rule: dfs_induct) case base then show ?case by simp next case (step S y xs) then show ?case by (auto simp add: visit_subset_dfs ins_eq ins_invariant succs_is_node) qed lemma succss_closed_dfs': "invariant ys ⟹ list_all is_node xs ⟹ succss (set_of ys) ⊆ set xs ∪ set_of ys ⟹ succss (set_of (dfs ys xs)) ⊆ set_of (dfs ys xs)" by (induct ys xs rule: dfs_induct) (auto simp add: ins_eq succss_def set_of_def cong: conj_cong) lemma succss_closed_dfs: "list_all is_node xs ⟹ succss (set_of (dfs empt xs)) ⊆ set_of (dfs empt xs)" apply (rule succss_closed_dfs') apply (rule empt_invariant) apply assumption apply (simp add: succss_def) apply (rule subsetI) apply (erule UN_E) apply (simp add: set_of_def empt cong: conj_cong) done lemma Image_closed_trancl: assumes "r `` X ⊆ X" shows "r⇧^{*}`` X = X" proof show "X ⊆ r⇧^{*}`` X" by auto show "r⇧^{*}`` X ⊆ X" proof - { fix x y assume y: "y ∈ X" assume "(y,x) ∈ r⇧^{*}" then have "x ∈ X" using assms y by induct (auto simp add: Image_def) } then show ?thesis by auto qed qed lemma reachable_closed_dfs: assumes "list_all is_node xs" shows "reachable (set xs) ⊆ set_of (dfs empt xs)" proof - from assms have "reachable (set xs) ⊆ reachable (set_of (dfs empt xs))" apply (unfold reachable_def) apply (rule Image_mono) apply (auto simp add: set_of_def next_subset_dfs empt_invariant list_all_iff) done also from succss_closed_dfs assms have "… = set_of (dfs empt xs)" apply (unfold reachable_def) apply (rule Image_closed_trancl) apply (auto simp add: succss_def set_of_def) done finally show ?thesis . qed lemma reachable_succs: "reachable (set (succs x)) ⊆ reachable {x}" by (auto simp add: reachable_def intro: converse_rtrancl_into_rtrancl) lemma dfs_subset_reachable_visit_nodes: "invariant ys ⟹ list_all is_node xs ⟹ set_of (dfs ys xs) ⊆ reachable (set xs) ∪ set_of ys" proof (induct ys xs rule: dfs_induct) case base then show ?case by (simp add: reachable_def) next case (step S x xs) show ?case proof (cases "memb x S") case True with step show ?thesis by (auto simp add: reachable_def) next case False have "reachable (set (succs x)) ⊆ reachable {x}" by (rule reachable_succs) then have "reachable (set (succs x @ xs)) ⊆ reachable (set (x # xs))" by (auto simp add: reachable_def) then show ?thesis using step by (auto simp add: reachable_def ins_eq set_of_def cong: conj_cong) qed qed theorem dfs_eq_reachable: assumes y: "is_node y" and xs: "list_all is_node xs" shows "memb y (dfs empt xs) = (y ∈ reachable (set xs))" proof assume "memb y (dfs empt xs)" with dfs_subset_reachable_visit_nodes [OF empt_invariant xs] y show "y ∈ reachable (set xs)" by (auto simp add: empt set_of_def) next assume "y ∈ reachable (set xs)" with reachable_closed_dfs [OF xs] show "memb y (dfs empt xs)" by (auto simp add: set_of_def) qed theorem dfs_eq_rtrancl: assumes y: "is_node y" and x: "is_node x" shows "memb y (dfs empt [x]) = ((x,y) ∈ (succsr succs)⇧^{*})" proof - from x have x': "list_all is_node [x]" by simp show ?thesis by (simp only: dfs_eq_reachable [OF y x'] reachable_def succsr_def) (auto simp add: empt) qed theorem dfs_invariant [consumes 2, case_names base step]: assumes S: "invariant S" and xs: "list_all is_node xs" and H: "I S" and I: "⋀S x. ¬ memb x S ⟹ is_node x ⟹ invariant S ⟹ I S ⟹ I (ins x S)" shows "I (dfs S xs)" proof - from S xs H have "I (dfs S xs) ∧ invariant (dfs S xs)" proof (induct S xs rule: dfs_induct) case base then show ?case by simp next case (step S x xs) show ?case proof (cases "memb x S") case True then show ?thesis by (simp add: step) next case False then show ?thesis apply simp apply (rule step) apply assumption apply (rule I) apply assumption apply (rule step)+ done qed qed then show ?thesis .. qed theorem dfs_invariant': "invariant S ⟹ list_all is_node xs ⟹ invariant (dfs S xs)" by (induct S xs rule: dfs_induct) auto theorem succsr_is_node: assumes "(x, y) ∈ (succsr succs)⇧^{*}" shows "is_node x ⟹ is_node y" using assms proof induct case base then show ?case . next case (step y z) then have "is_node y" by simp then have "list_all is_node (succs y)" by (rule succs_is_node) with step show ?case by (simp add: succsr_def list_all_iff) qed end declare gen_dfs_simps [simp del] end

# Theory Presburger_Automata

(* Title: Presburger-Automata/Presburger_Automata.thy Author: Markus Reiter and Stefan Berghofer, TU Muenchen, 2008-2009 *) theory Presburger_Automata imports DFS "HOL-Library.Nat_Bijection" begin section ‹General automata› definition "reach tr p as q = (q = foldl tr p as)" lemma reach_nil: "reach tr p [] p" by (simp add: reach_def) lemma reach_snoc: "reach tr p bs q ⟹ reach tr p (bs @ [b]) (tr q b)" by (simp add: reach_def) lemma reach_nil_iff: "reach tr p [] q = (p = q)" by (auto simp add: reach_def) lemma reach_snoc_iff: "reach tr p (bs @ [b]) k = (∃q. reach tr p bs q ∧ k = tr q b)" by (auto simp add: reach_def) lemma reach_induct [consumes 1, case_names Nil snoc, induct set: reach]: assumes "reach tr p w q" and "P [] p" and "⋀k x y. ⟦reach tr p x k; P x k⟧ ⟹ P (x @ [y]) (tr k y)" shows "P w q" using assms by (induct w arbitrary: q rule: rev_induct) (simp add: reach_def)+ lemma reach_trans: "⟦reach tr p a r; reach tr r b q⟧ ⟹ reach tr p (a @ b) q" by (simp add: reach_def) lemma reach_inj: "⟦reach tr p a q; reach tr p a q'⟧ ⟹ q = q'" by (simp add: reach_def) definition "accepts tr P s as = P (foldl tr s as)" locale Automaton = fixes trans :: "'a ⇒ 'b ⇒ 'a" and is_node :: "'a ⇒ bool" and is_alpha :: "'b ⇒ bool" assumes trans_is_node: "⋀q a. ⟦is_node q; is_alpha a⟧ ⟹ is_node (trans q a)" begin lemma steps_is_node: assumes "is_node q" and "list_all is_alpha w" shows "is_node (foldl trans q w)" using assms by (induct w arbitrary: q) (simp add: trans_is_node)+ lemma reach_is_node: "⟦reach trans p w q; is_node p; list_all is_alpha w⟧ ⟹ is_node q" by (simp add: steps_is_node reach_def) end section ‹BDDs› definition is_alph :: "nat ⇒ bool list ⇒ bool" where "is_alph n = (λw. length w = n)" datatype 'a bdd = Leaf 'a | Branch "'a bdd" "'a bdd" for map: bdd_map primrec bddh :: "nat ⇒ 'a bdd ⇒ bool" where "bddh n (Leaf x) = True" | "bddh n (Branch l r) = (case n of 0 ⇒ False | Suc m ⇒ bddh m l ∧ bddh m r)" lemma bddh_ge: assumes "m ≥ n" assumes "bddh n bdd" shows "bddh m bdd" using assms proof (induct bdd arbitrary: n m) case (Branch l r) then obtain v where V: "n = Suc v" by (cases n) simp+ show ?case proof (cases "n = m") case True with Branch show ?thesis by simp next case False with Branch have "∃w. m = Suc w ∧ n ≤ w" by (cases m) simp+ then obtain w where W: "m = Suc w ∧ n ≤ w" .. with Branch V have "v ≤ w ∧ bddh v l ∧ bddh v r" by simp with Branch have "bddh w l ∧ bddh w r" by blast with W show ?thesis by simp qed qed simp abbreviation "bdd_all ≡ pred_bdd" fun bdd_lookup :: "'a bdd ⇒ bool list ⇒ 'a" where "bdd_lookup (Leaf x) bs = x" | "bdd_lookup (Branch l r) (b#bs) = bdd_lookup (if b then r else l) bs" lemma bdd_all_bdd_lookup: "⟦bddh (length ws) bdd; bdd_all P bdd⟧ ⟹ P (bdd_lookup bdd ws)" by (induct bdd ws rule: bdd_lookup.induct) simp+ lemma bdd_all_bdd_lookup_iff: "bddh n bdd ⟹ bdd_all P bdd = (∀ws. length ws = n ⟶ P (bdd_lookup bdd ws))" apply (rule iffI) apply (simp add: bdd_all_bdd_lookup) proof (induct bdd arbitrary: n) case Leaf thus ?case apply simp apply (erule mp) apply (rule_tac x="replicate n False" in exI, simp) done next case (Branch l r n) then obtain k where k: "n = Suc k" by (cases n) simp+ from Branch have R: "⋀ws. length ws = n ⟹ P (bdd_lookup (Branch l r) ws)" by simp have "⋀ws. length ws = k ⟹ P (bdd_lookup l ws) ∧ P (bdd_lookup r ws)" proof - fix ws :: "bool list" assume H: "length ws = k" with k have "length (False#ws) = n" by simp hence 1: "P (bdd_lookup (Branch l r) (False#ws))" by (rule R) from H k have "length (True#ws) = n" by simp hence "P (bdd_lookup (Branch l r) (True#ws))" by (rule R) with 1 show "P (bdd_lookup l ws) ∧ P (bdd_lookup r ws)" by simp qed with Branch k show ?case by auto qed lemma bdd_all_bdd_map: assumes "bdd_all P bdd" and "⋀a. P a ⟹ Q (f a)" shows "bdd_all Q (bdd_map f bdd)" using assms by (induct bdd) simp+ lemma bddh_bdd_map: shows "bddh n (bdd_map f bdd) = bddh n bdd" proof assume "bddh n (bdd_map f bdd)" thus "bddh n bdd" proof (induct bdd arbitrary: n) case (Branch l r n) then obtain k where "n = Suc k" by (cases n) simp+ with Branch show ?case by simp qed simp next assume "bddh n bdd" thus "bddh n (bdd_map f bdd)" proof (induct bdd arbitrary: n) case (Branch l r n) then obtain k where "n = Suc k" by (cases n) simp+ with Branch show ?case by simp qed simp qed lemma bdd_map_bdd_lookup: assumes "bddh (length ws) bdd" shows "bdd_lookup (bdd_map f bdd) ws = f (bdd_lookup bdd ws)" using assms by (induct bdd ws rule: bdd_lookup.induct) (auto simp add: bddh_bdd_map)+ fun bdd_binop :: "('a ⇒ 'b ⇒ 'c) ⇒ 'a bdd ⇒ 'b bdd ⇒ 'c bdd" where "bdd_binop f (Leaf x) (Leaf y) = Leaf (f x y)" | "bdd_binop f (Branch l r) (Leaf y) = Branch (bdd_binop f l (Leaf y)) (bdd_binop f r (Leaf y))" | "bdd_binop f (Leaf x) (Branch l r) = Branch (bdd_binop f (Leaf x) l) (bdd_binop f (Leaf x) r)" | "bdd_binop f (Branch l⇩_{1}r⇩_{1}) (Branch l⇩_{2}r⇩_{2}) = Branch (bdd_binop f l⇩_{1}l⇩_{2}) (bdd_binop f r⇩_{1}r⇩_{2})" lemma bddh_binop: "bddh n (bdd_binop f l r) = (bddh n l ∧ bddh n r)" by (induct f l r arbitrary: n rule: bdd_binop.induct) (auto split: nat.split_asm) lemma bdd_lookup_binop: "⟦bddh (length bs) l; bddh (length bs) r⟧ ⟹ bdd_lookup (bdd_binop f l r) bs = f (bdd_lookup l bs) (bdd_lookup r bs)" apply (induct f l r arbitrary: bs rule: bdd_binop.induct) apply simp apply (case_tac bs) apply simp+ apply (case_tac bs) apply simp+ apply (case_tac bs) apply simp+ done lemma bdd_all_bdd_binop: assumes "bdd_all P bdd" and "bdd_all Q bdd'" and "⋀a b. ⟦P a; Q b⟧ ⟹ R (f a b)" shows "bdd_all R (bdd_binop f bdd bdd')" using assms by (induct f bdd bdd' rule: bdd_binop.induct) simp+ lemma insert_list_idemp[simp]: "List.insert x (List.insert x xs) = List.insert x xs" by simp primrec add_leaves :: "'a bdd ⇒ 'a list ⇒ 'a list" where "add_leaves (Leaf x) xs = List.insert x xs" | "add_leaves (Branch b c) xs = add_leaves c (add_leaves b xs)" 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]) ⊆ (⋃x∈set (add_leaves b xs). ⋃y∈set (add_leaves b' ys). {f x y})" (is "?A ⊆ ?B") proof - have "?A ⊆ (⋃x∈set (add_leaves b xs). f x ` set (add_leaves b' ys))" proof (induct f b b' arbitrary: xs ys rule: bdd_binop.induct) case (1 f x y xs ys) then show ?case by auto next case (2 f l r y xs ys) then show ?case apply auto apply (drule_tac ys1="[f x y. x ← add_leaves l xs, y ← List.insert y ys]" in rev_subsetD [OF _ add_leaves_mono]) apply auto apply (drule meta_spec, drule meta_spec, drule subsetD, assumption) apply simp done next case (3 f x l r xs ys) then show ?case apply auto apply (drule_tac ys1="[f x y. x ← List.insert x xs, y ← add_leaves l ys]" in rev_subsetD [OF _ add_leaves_mono]) apply auto apply (drule meta_spec, drule meta_spec, drule subsetD, assumption) apply simp done next case (4 f l⇩_{1}r⇩_{1}l⇩_{2}r⇩_{2}xs ys) then show ?case apply auto apply (drule_tac ys1="[f x y. x ← add_leaves l⇩_{1}xs, y ← add_leaves l⇩_{2}ys]" in rev_subsetD [OF _ add_leaves_mono]) apply simp apply (drule meta_spec, drule meta_spec, drule subsetD, assumption) apply simp done qed also have "(⋃x∈set (add_leaves b xs). f x ` set (add_leaves b' ys)) = ?B" by auto finally show ?thesis . qed section ‹DFAs› type_synonym bddtable = "nat bdd list" type_synonym astate = "bool list" type_synonym dfa = "bddtable × astate" definition dfa_is_node :: "dfa ⇒ nat ⇒ bool" where "dfa_is_node A = (λq. q < length (fst A))" definition wf_dfa :: "dfa ⇒ nat ⇒ bool" where "wf_dfa A n = (list_all (bddh n) (fst A) ∧ list_all (bdd_all (dfa_is_node A)) (fst A) ∧ length (snd A) = length (fst A) ∧ length (fst A) > 0)" definition dfa_trans :: "dfa ⇒ nat ⇒ bool list ⇒ nat" where "dfa_trans A q bs ≡ bdd_lookup (fst A ! q) bs" definition dfa_accepting :: "dfa ⇒ nat ⇒ bool" where "dfa_accepting A q = snd A ! q" locale aut_dfa = fixes A n assumes well_formed: "wf_dfa A n" sublocale aut_dfa < Automaton "dfa_trans A" "dfa_is_node A" "is_alph n" proof fix q a assume Q: "dfa_is_node A q" and A: "is_alph n a" hence QL: "q < length (fst A)" by (simp add: dfa_is_node_def) with well_formed A have H: "bddh (length a) (fst A ! q)" by (simp add: wf_dfa_def list_all_iff is_alph_def) from QL well_formed have "bdd_all (dfa_is_node A) (fst A ! q)" by (simp add: wf_dfa_def list_all_iff) with H show "dfa_is_node A (dfa_trans A q a)" by (simp add: dfa_trans_def bdd_all_bdd_lookup) qed context aut_dfa begin lemmas trans_is_node = trans_is_node lemmas steps_is_node = steps_is_node lemmas reach_is_node = reach_is_node end lemmas dfa_trans_is_node = aut_dfa.trans_is_node [OF aut_dfa.intro] lemmas dfa_steps_is_node = aut_dfa.steps_is_node [OF aut_dfa.intro] lemmas dfa_reach_is_node = aut_dfa.reach_is_node [OF aut_dfa.intro] abbreviation "dfa_steps A ≡ foldl (dfa_trans A)" abbreviation "dfa_accepts A ≡ accepts (dfa_trans A) (dfa_accepting A) 0" abbreviation "dfa_reach A ≡ reach (dfa_trans A)" lemma dfa_startnode_is_node: "wf_dfa A n ⟹ dfa_is_node A 0" by (simp add: dfa_is_node_def wf_dfa_def) subsection ‹Minimization› primrec make_tr :: "(nat ⇒ 'a) ⇒ nat ⇒ nat ⇒ 'a list" where "make_tr f 0 i = []" | "make_tr f (Suc n) i = f i # make_tr f n (Suc i)" primrec fold_map_idx :: "(nat ⇒ 'c ⇒ 'a ⇒ 'c × 'b) ⇒ nat ⇒ 'c ⇒ 'a list ⇒ 'c × 'b list" where "fold_map_idx f i y [] = (y, [])" | "fold_map_idx f i y (x # xs) = (let (y', x') = f i y x in let (y'', xs') = fold_map_idx f (Suc i) y' xs in (y'', x' # xs'))" definition init_tr :: "dfa ⇒ bool list list" where "init_tr = (λ(bd,as). make_tr (λi. make_tr (λj. as ! i ≠ as ! j) i 0) (length bd - 1) 1)" definition tr_lookup :: "bool list list ⇒ nat ⇒ nat ⇒ bool" where "tr_lookup = (λT i j. (if i = j then False else if i > j then T ! (i - 1) ! j else T ! (j - 1) ! i))" fun check_eq :: "nat bdd ⇒ nat bdd ⇒ bool list list ⇒ bool" where "check_eq (Leaf i) (Leaf j) T = (¬ tr_lookup T i j)" | "check_eq (Branch l r) (Leaf i) T = (check_eq l (Leaf i) T ∧ check_eq r (Leaf i) T)" | "check_eq (Leaf i) (Branch l r) T = (check_eq (Leaf i) l T ∧ check_eq (Leaf i) r T)" | "check_eq (Branch l1 r1) (Branch l2 r2) T = (check_eq l1 l2 T ∧ check_eq r1 r2 T)" definition iter :: "dfa ⇒ bool list list ⇒ bool × bool list list" where "iter = (λ(bd,as) T. fold_map_idx (λi. fold_map_idx (λj c b. let b' = b ∨ ¬ check_eq (bd ! i) (bd ! j) T in (c ∨ b ≠ b', b')) 0) 1 False T)" definition count_tr :: "bool list list ⇒ nat" where "count_tr = foldl (foldl (λy x. if x then y else Suc y)) 0" lemma fold_map_idx_fst_snd_eq: assumes f: "⋀i c x. fst (f i c x) = (c ∨ x ≠ snd (f i c x))" shows "fst (fold_map_idx f i c xs) = (c ∨ xs ≠ snd (fold_map_idx f i c xs))" by (induct xs arbitrary: i c) (simp_all add: split_beta f) lemma foldl_mono: assumes f: "⋀x y y'. y < y' ⟹ f y x < f y' x" and y: "y < y'" shows "foldl f y xs < foldl f y' xs" using y by (induct xs arbitrary: y y') (simp_all add: f) lemma fold_map_idx_count: assumes f: "⋀i c x y. fst (f i c x) = (c ∨ g y (snd (f i c x)) < (g y x::nat))" and f': "⋀i c x y. g y (snd (f i c x)) ≤ g y x" and g: "⋀x y y'. y < y' ⟹ g y x < g y' x" shows "fst (fold_map_idx f i c xs) = (c ∨ foldl g y (snd (fold_map_idx f i c xs)) < foldl g y xs)" and "foldl g y (snd (fold_map_idx f i c xs)) ≤ foldl g y xs" proof (induct xs arbitrary: i c y) case (Cons x xs) { case 1 show ?case using f' [of y i c x, simplified le_eq_less_or_eq] by (auto simp add: split_beta Cons(1) [of _ _ "g y (snd (f i c x))"] f [of _ _ _ y] intro: less_le_trans foldl_mono g Cons) next case 2 show ?case using f' [of y i c x, simplified le_eq_less_or_eq] by (auto simp add: split_beta intro: order_trans less_imp_le intro!: foldl_mono g Cons) } qed simp_all lemma iter_count: assumes eq: "(b, T') = iter (bd, as) T" and b: "b" shows "count_tr T' < count_tr T" proof - let ?f = "fold_map_idx (λi. fold_map_idx (λj c b. let b' = b ∨ ¬ check_eq (bd ! i) (bd ! j) T in (c ∨ b ≠ b', b')) 0) (Suc 0) False T" from eq [symmetric] b have "fst ?f" by (auto simp add: iter_def) also have "fst ?f = (False ∨ count_tr (snd ?f) < count_tr T)" unfolding count_tr_def by (rule fold_map_idx_count foldl_mono | simp)+ finally show ?thesis by (simp add: eq [THEN arg_cong, of snd, simplified] iter_def) qed function fixpt :: "dfa ⇒ bool list list ⇒ bool list list" where "fixpt M T = (let (b, T2) = iter M T in if b then fixpt M T2 else T2)" by auto termination by (relation "measure (λ(M, T). count_tr T)") (auto simp: iter_count) lemma fixpt_True[simp]: "fst (iter M T) ⟹ fixpt M T = fixpt M (snd (iter M T))" by (simp add: split_beta) lemma fixpt_False[simp]: "¬ (fst (iter M T)) ⟹ fixpt M T = T" by (simp add: split_beta iter_def fold_map_idx_fst_snd_eq) declare fixpt.simps [simp del] lemma fixpt_induct: assumes H: "⋀M T. (fst (iter M T) ⟹ P M (snd (iter M T))) ⟹ P M T" shows "P M T" proof (induct M T rule: fixpt.induct) case (1 M T) show ?case by (rule H) (rule 1 [OF refl prod.collapse]) qed definition dist_nodes :: "dfa ⇒ nat ⇒ nat ⇒ nat ⇒ nat ⇒ bool" where "dist_nodes = (λM n m p q. ∃w. length w = n ∧ list_all (is_alph m) w ∧ dfa_accepting M (dfa_steps M p w) ≠ dfa_accepting M (dfa_steps M q w))" definition wf_tr :: "dfa ⇒ bool list list ⇒ bool" where "wf_tr = (λM T. length T = length (fst M) - 1 ∧ (∀i < length T. length (T ! i) = i + 1))" lemma make_tr_len: "length (make_tr f n i) = n" by (induct n arbitrary: i) simp_all lemma make_tr_nth: "j < n ⟹ make_tr f n i ! j = f (i + j)" by (induct n arbitrary: i j) (auto simp add: nth_Cons') lemma init_tr_wf: "wf_tr M (init_tr M)" by (simp add: init_tr_def wf_tr_def split_beta make_tr_len make_tr_nth) lemma fold_map_idx_len: "length (snd (fold_map_idx f i y xs)) = length xs" by (induct xs arbitrary: i y) (simp_all add: split_beta) lemma fold_map_idx_nth: "j < length xs ⟹ snd (fold_map_idx f i y xs) ! j = snd (f (i + j) (fst (fold_map_idx f i y (take j xs))) (xs ! j))" by (induct xs arbitrary: i j y) (simp_all add: split_beta nth_Cons' take_Cons') lemma init_tr_dist_nodes: assumes "dfa_is_node M q" and "p < q" shows "tr_lookup (init_tr M) q p = dist_nodes M 0 v p q" proof - have 1: "dist_nodes M 0 v p q = (snd M ! p ≠ snd M ! q)" by (simp add: dist_nodes_def dfa_accepting_def) from assms have "tr_lookup (init_tr M) q p = (snd M ! p ≠ snd M ! q)" by (auto simp add: dfa_is_node_def init_tr_def tr_lookup_def make_tr_nth split_beta) with 1 show ?thesis by simp qed lemma dist_nodes_suc: "dist_nodes M (Suc n) v p q = (∃bs. is_alph v bs ∧ dist_nodes M n v (dfa_trans M p bs) (dfa_trans M q bs))" proof assume "dist_nodes M (Suc n) v p q" then obtain w where W: "length w = Suc n" and L: "list_all (is_alph v) w" and A: "dfa_accepting M (dfa_steps M p w) ≠ dfa_accepting M (dfa_steps M q w)" unfolding dist_nodes_def by blast then obtain b bs where B: "w = b # bs" by (cases w) auto from A have A2: "dfa_accepting M (dfa_steps M (dfa_trans M p b) bs) ≠ dfa_accepting M (dfa_steps M (dfa_trans M q b) bs)" unfolding B by simp with W B L show "∃bs. is_alph v bs ∧ dist_nodes M n v (dfa_trans M p bs) (dfa_trans M q bs)" by (auto simp: dist_nodes_def) next assume "∃bs. is_alph v bs ∧ dist_nodes M n v (dfa_trans M p bs) (dfa_trans M q bs)" then obtain b bs where W: "length bs = n" and V: "is_alph v b" and V': "list_all (is_alph v) bs" and A: "dfa_accepting M (dfa_steps M (dfa_trans M p b) bs) ≠ dfa_accepting M (dfa_steps M (dfa_trans M q b) bs)" unfolding dist_nodes_def by blast hence "dfa_accepting M (dfa_steps M p (b # bs)) ≠ dfa_accepting M (dfa_steps M q (b # bs))" by simp moreover from W have "length (b # bs) = Suc n" by simp moreover from V V' have "list_all (is_alph v) (b # bs)" by simp ultimately show "dist_nodes M (Suc n) v p q" unfolding dist_nodes_def by blast qed lemma bdd_lookup_append: assumes "bddh n B" and "length bs ≥ n" shows "bdd_lookup B (bs @ w) = bdd_lookup B bs" using assms proof (induct B bs arbitrary: n rule: bdd_lookup.induct) case (2 l r b bs n) then obtain n' where N: "n = Suc n'" by (cases n) simp+ with 2 show ?case by (cases b) auto qed simp+ lemma bddh_exists: "∃n. bddh n B" proof (induct B) case (Branch l r) then obtain n m where L: "bddh n l" and R: "bddh m r" by blast with bddh_ge[of n "max n m" l] bddh_ge[of m "max n m" r] have "bddh (Suc (max n m)) (Branch l r)" by simp thus ?case by (rule exI) qed simp lemma check_eq_dist_nodes: assumes "∀p q. dfa_is_node M q ∧ p < q ⟶ tr_lookup T q p = (∃n < m. dist_nodes M n v p q)" and "m > 0" and "bdd_all (dfa_is_node M) l" and "bdd_all (dfa_is_node M) r" shows "(¬ check_eq l r T) = (∃bs. bddh (length bs) l ∧ bddh (length bs) r ∧ (∃n < m. dist_nodes M n v (bdd_lookup l bs) (bdd_lookup r bs)))" using assms proof (induct l r T rule: check_eq.induct) case (1 i j T) have "i < j ∨ i = j ∨ i > j" by auto thus ?case by (elim disjE) (insert 1, auto simp: dist_nodes_def tr_lookup_def) next case (2 l r i T) hence IV1: "(¬ check_eq l (Leaf i) T) = (∃bs. bddh (length bs) l ∧ bddh (length bs) (Leaf i) ∧ (∃n<m. dist_nodes M n v (bdd_lookup l bs) (bdd_lookup (Leaf i) bs)))" by simp from 2 have IV2: "(¬ check_eq r (Leaf i) T) = (∃bs. bddh (length bs) r ∧ bddh (length bs) (Leaf i) ∧ (∃n<m. dist_nodes M n v (bdd_lookup r bs) (bdd_lookup (Leaf i) bs)))" by simp have "(¬ check_eq (Branch l r) (Leaf i) T) = (¬ check_eq l (Leaf i) T ∨ ¬ check_eq r (Leaf i) T)" by simp also have "… = (∃bs. bddh (length bs) (Branch l r) ∧ bddh (length bs) (Leaf i) ∧ (∃n<m . dist_nodes M n v (bdd_lookup (Branch l r) bs) (bdd_lookup (Leaf i) bs)))" (is "(?L ∨ ?R) = ?E") proof assume "?L ∨ ?R" thus "?E" proof (elim disjE) assume "?L" then obtain bs where O: "bddh (length bs) l ∧ bddh (length bs) (Leaf i) ∧ (∃n<m. dist_nodes M n v (bdd_lookup l bs) (bdd_lookup (Leaf i) bs))" unfolding IV1 by blast from bddh_exists obtain k where B: "bddh k r" by blast with O have "bddh (length bs + k) r" and "bddh (length bs + k) l" and "bddh (length bs + k) (Leaf i)" by (simp add: bddh_ge[of k "length bs + k"] bddh_ge[of "length bs" "length bs + k"])+ with O have "bddh (length (False # bs @ replicate k False)) (Branch l r) ∧ bddh (length (False # bs @ replicate k False)) (Leaf i) ∧ (∃n<m. dist_nodes M n v (bdd_lookup (Branch l r) (False # bs @ replicate k False)) (bdd_lookup (Leaf i) (False # bs @ replicate k False)))" by (auto simp: bdd_lookup_append) thus ?thesis by (rule exI) next assume "?R" then obtain bs where O: "bddh (length bs) r ∧ bddh (length bs) (Leaf i) ∧ (∃n<m. dist_nodes M n v (bdd_lookup r bs) (bdd_lookup (Leaf i) bs))" unfolding IV2 by blast from bddh_exists obtain k where B: "bddh k l" by blast with O have "bddh (length bs + k) l" and "bddh (length bs + k) r" and "bddh (length bs + k) (Leaf i)" by (simp add: bddh_ge[of k "length bs + k"] bddh_ge[of "length bs" "length bs + k"])+ with O have "bddh (length (True # bs @ replicate k False)) (Branch l r) ∧ bddh (length (True # bs @ replicate k False)) (Leaf i) ∧ (∃n<m. dist_nodes M n v (bdd_lookup (Branch l r) (True # bs @ replicate k False)) (bdd_lookup (Leaf i) (True # bs @ replicate k False)))" by (auto simp: bdd_lookup_append) thus ?thesis by (rule exI) qed next assume "?E" then obtain bs where O: "bddh (length bs) (Branch l r) ∧ bddh (length bs) (Leaf i) ∧ (∃n<m. dist_nodes M n v (bdd_lookup (Branch l r) bs) (bdd_lookup (Leaf i) bs))" by blast then obtain b br where B: "bs = b # br" by (cases bs) auto with O IV1 IV2 show "?L ∨ ?R" by (cases b) auto qed finally show ?case by simp next case (3 i l r T) hence IV1: "(¬ check_eq (Leaf i) l T) = (∃bs. bddh (length bs) l ∧ bddh (length bs) (Leaf i) ∧ (∃n<m. dist_nodes M n v (bdd_lookup (Leaf i) bs) (bdd_lookup l bs)))" by simp from 3 have IV2: "(¬ check_eq (Leaf i) r T) = (∃bs. bddh (length bs) r ∧ bddh (length bs) (Leaf i) ∧ (∃n<m. dist_nodes M n v (bdd_lookup (Leaf i) bs) (bdd_lookup r bs)))" by simp have "(¬ check_eq (Leaf i) (Branch l r) T) = (¬ check_eq (Leaf i) l T ∨ ¬ check_eq (Leaf i) r T)" by simp also have "… = (∃bs. bddh (length bs) (Branch l r) ∧ bddh (length bs) (Leaf i) ∧ (∃n<m . dist_nodes M n v (bdd_lookup (Leaf i) bs) (bdd_lookup (Branch l r) bs)))" (is "(?L ∨ ?R) = ?E") proof assume "?L ∨ ?R" thus "?E" proof (elim disjE) assume "?L" then obtain bs where O: "bddh (length bs) l ∧ bddh (length bs) (Leaf i) ∧ (∃n<m. dist_nodes M n v (bdd_lookup (Leaf i) bs) (bdd_lookup l bs))" unfolding IV1 by blast from bddh_exists obtain k where B: "bddh k r" by blast with O have "bddh (length bs + k) r" and "bddh (length bs + k) l" and "bddh (length bs + k) (Leaf i)" by (simp add: bddh_ge[of k "length bs + k"] bddh_ge[of "length bs" "length bs + k"])+ with O have "bddh (length (False # bs @ replicate k False)) (Branch l r) ∧ bddh (length (False # bs @ replicate k False)) (Leaf i) ∧ (∃n<m. dist_nodes M n v (bdd_lookup (Leaf i) (False # bs @ replicate k False)) (bdd_lookup (Branch l r) (False # bs @ replicate k False)))" by (auto simp: bdd_lookup_append) thus ?thesis by (rule exI) next assume "?R" then obtain bs where O: "bddh (length bs) r ∧ bddh (length bs) (Leaf i) ∧ (∃n<m. dist_nodes M n v (bdd_lookup (Leaf i) bs) (bdd_lookup r bs))" unfolding IV2 by blast from bddh_exists obtain k where B: "bddh k l" by blast with O have "bddh (length bs + k) l" and "bddh (length bs + k) r" and "bddh (length bs + k) (Leaf i)" by (simp add: bddh_ge[of k "length bs + k"] bddh_ge[of "length bs" "length bs + k"])+ with O have "bddh (length (True # bs @ replicate k False)) (Branch l r) ∧ bddh (length (True # bs @ replicate k False)) (Leaf i) ∧ (∃n<m. dist_nodes M n v (bdd_lookup (Leaf i) (True # bs @ replicate k False)) (bdd_lookup (Branch l r) (True # bs @ replicate k False)))" by (auto simp: bdd_lookup_append) thus ?thesis by (rule exI) qed next assume "?E" then obtain bs where O: "bddh (length bs) (Branch l r) ∧ bddh (length bs) (Leaf i) ∧ (∃n<m. dist_nodes M n v (bdd_lookup (Leaf i) bs) (bdd_lookup (Branch l r) bs))" by blast then obtain b br where B: "bs = b # br" by (cases bs) auto with O IV1 IV2 show "?L ∨ ?R" by (cases b) auto qed finally show ?case by simp next case (4 l1 r1 l2 r2 T) hence IV1: "(¬ check_eq l1 l2 T) = (∃bs. bddh (length bs) l1 ∧ bddh (length bs) l2 ∧ (∃n<m. dist_nodes M n v (bdd_lookup l1 bs) (bdd_lookup l2 bs)))" by simp from 4 have IV2: "(¬ check_eq r1 r2 T) = (∃bs. bddh (length bs) r1 ∧ bddh (length bs) r2 ∧ (∃n<m. dist_nodes M n v (bdd_lookup r1 bs) (bdd_lookup r2 bs)))" by simp have "(¬ check_eq (Branch l1 r1) (Branch l2 r2) T) = (¬ check_eq l1 l2 T ∨ ¬ check_eq r1 r2 T)" by simp also have "… = (∃bs. bddh (length bs) (Branch l1 r1) ∧ bddh (length bs) (Branch l2 r2) ∧ (∃n<m. dist_nodes M n v (bdd_lookup (Branch l1 r1) bs) (bdd_lookup (Branch l2 r2) bs)))" (is "(?L ∨ ?R) = (∃bs. ?E bs)") proof assume "?L ∨ ?R" thus "∃bs. ?E bs" proof (elim disjE) assume "?L" then obtain bs where O: "bddh (length bs) l1 ∧ bddh (length bs) l2 ∧ (∃n<m. dist_nodes M n v (bdd_lookup l1 bs) (bdd_lookup l2 bs))" unfolding IV1 by blast from bddh_exists obtain k1 k2 where K1: "bddh k1 r1" and K2: "bddh k2 r2" by blast with O have "bddh (length bs + max k1 k2) l1" and "bddh (length bs + max k1 k2) l2" and "bddh (length bs + max k1 k2) r1" and "bddh (length bs + max k1 k2) r2" by (simp add: bddh_ge[of "length bs" "length bs + max k1 k2"] bddh_ge[of k1 "length bs + max k1 k2"] bddh_ge[of k2 "length bs + max k1 k2"])+ with O have "bddh (length (False # bs @ replicate (max k1 k2) False)) (Branch l1 r1) ∧ bddh (length (False # bs @ replicate (max k1 k2) False)) (Branch l2 r2) ∧ (∃n<m. dist_nodes M n v (bdd_lookup (Branch l1 r1) (False # bs @ replicate (max k1 k2) False)) (bdd_lookup (Branch l2 r2) (False # bs @ replicate (max k1 k2) False)))" by (auto simp: bdd_lookup_append) thus ?thesis by (rule exI) next assume "?R" then obtain bs where O: "bddh (length bs) r1 ∧ bddh (length bs) r2 ∧ (∃n<m. dist_nodes M n v (bdd_lookup r1 bs) (bdd_lookup r2 bs))" unfolding IV2 by blast from bddh_exists obtain k1 k2 where K1: "bddh k1 l1" and K2: "bddh k2 l2" by blast with O have "bddh (length bs + max k1 k2) l1" and "bddh (length bs + max k1 k2) l2" and "bddh (length bs + max k1 k2) r1" and "bddh (length bs + max k1 k2) r2" by (simp add: bddh_ge[of "length bs" "length bs + max k1 k2"] bddh_ge[of k1 "length bs + max k1 k2"] bddh_ge[of k2 "length bs + max k1 k2"])+ with O have "bddh (length (True # bs @ replicate (max k1 k2) False)) (Branch l1 r1) ∧ bddh (length (True # bs @ replicate (max k1 k2) False)) (Branch l2 r2) ∧ (∃n<m. dist_nodes M n v (bdd_lookup (Branch l1 r1) (True # bs @ replicate (max k1 k2) False)) (bdd_lookup (Branch l2 r2) (True # bs @ replicate (max k1 k2) False)))" by (auto simp: bdd_lookup_append) thus ?thesis by (rule exI) qed next assume "∃bs. ?E bs" then obtain bs where O: "?E bs" by blast then obtain b br where B: "bs = b # br" by (cases bs) auto with O IV1 IV2 show "?L ∨ ?R" by (cases b) auto qed finally show ?case by simp qed lemma iter_wf: "wf_tr M T ⟹ wf_tr M (snd (iter M T))" by (simp add: wf_tr_def iter_def fold_map_idx_len fold_map_idx_nth split_beta) lemma fixpt_wf: "wf_tr M T ⟹ wf_tr M (fixpt M T)" proof (induct M T rule: fixpt_induct) case (1 M T) show ?case proof (cases "fst (iter M T)") case True with 1 show ?thesis by (simp add: iter_wf) next case False with 1 show ?thesis by simp qed qed lemma list_split: assumes "n ≤ length bss" shows "∃b bs. bss = b @ bs ∧ length b = n" using assms proof (induct bss arbitrary: n) case (Cons a as) show ?case proof (cases n) case (Suc n') with Cons have "∃b bs. as = b @ bs ∧ length b = n'" by simp then obtain b bs where B: "as = b @ bs ∧ length b = n'" by blast with Suc Cons have "a # as = (a # b) @ bs ∧ length (a # b) = n" by simp thus ?thesis by blast qed simp qed simp lemma iter_dist_nodes: assumes "wf_tr M T" and "wf_dfa M v" and "∀p q. dfa_is_node M q ∧ p < q ⟶ tr_lookup T q p = (∃n < m. dist_nodes M n v p q)" and "m > 0" and "dfa_is_node M q" and "p < q" shows "tr_lookup (snd (iter M T)) q p = (∃n < Suc m. dist_nodes M n v p q)" proof - from assms obtain m' where M': "m = Suc m'" by (cases m) simp+ have C: "(¬ check_eq (fst M ! q) (fst M ! p) T) = (∃n<m. dist_nodes M (Suc n) v p q)" proof assume "¬ check_eq (fst M ! q) (fst M ! p) T" with assms have "∃bs. bddh (length bs) (fst M ! q) ∧ bddh (length bs) (fst M ! p) ∧ (∃n < m. dist_nodes M n v (bdd_lookup (fst M ! q) bs) (bdd_lookup (fst M ! p) bs))" by (simp add: check_eq_dist_nodes wf_dfa_def list_all_iff dfa_is_node_def) then obtain bs n bss where X: "bddh (length bs) (fst M ! q) ∧ bddh (length bs) (fst M ! p) ∧ n < m ∧ length bss = n ∧ list_all (is_alph v) bss ∧ dfa_accepting M (dfa_steps M (bdd_lookup (fst M ! q) bs) bss) ≠ dfa_accepting M (dfa_steps M (bdd_lookup (fst M ! p) bs) bss)" unfolding dist_nodes_def by blast from list_split[of v "bs @ replicate v False"] have "∃b' bs'. bs @ replicate v False = b' @ bs' ∧ length b' = v" by simp then obtain b' bs' where V: "bs @ replicate v False = b' @ bs' ∧ length b' = v" by blast with X bdd_lookup_append[of "length bs" "fst M ! q" "bs" "replicate v False"] bdd_lookup_append[of "length bs" "fst M ! p" "bs" "replicate v False"] have 1: "dfa_accepting M (dfa_steps M (bdd_lookup (fst M ! q) (bs @ replicate v False)) bss) ≠ dfa_accepting M (dfa_steps M (bdd_lookup (fst M ! p) (bs @ replicate v False)) bss)" by simp from assms have "bddh v (fst M ! q) ∧ bddh v (fst M ! p)" by (simp add: wf_dfa_def dfa_is_node_def list_all_iff) with 1 V have "dfa_accepting M (dfa_steps M (dfa_trans M q b') bss) ≠ dfa_accepting M (dfa_steps M (dfa_trans M p b') bss)" by (auto simp: bdd_lookup_append dfa_trans_def) with X V have "is_alph v b' ∧ dist_nodes M n v (dfa_trans M p b') (dfa_trans M q b')" by (auto simp: dist_nodes_def is_alph_def) hence "dist_nodes M (Suc n) v p q" by (auto simp: dist_nodes_suc) with X show "∃n<m. dist_nodes M (Suc n) v p q" by auto next assume "∃n<m. dist_nodes M (Suc n) v p q" hence "∃bs. ∃n<m. is_alph v bs ∧ dist_nodes M n v (dfa_trans M p bs) (dfa_trans M q bs)" by (auto simp: dist_nodes_suc) then obtain bs where X: "∃n<m. is_alph v bs ∧ dist_nodes M n v (dfa_trans M p bs) (dfa_trans M q bs)" by blast hence BS: "length bs = v" by (auto simp: is_alph_def) with assms have "bddh (length bs) (fst M ! p) ∧ bddh (length bs) (fst M ! q)" by (simp add: wf_dfa_def dfa_is_node_def list_all_iff) with X have "bddh (length bs) (fst M ! p) ∧ bddh (length bs) (fst M ! q) ∧ (∃n<m. dist_nodes M n v (bdd_lookup (fst M ! q) bs) (bdd_lookup (fst M ! p) bs))" by (auto simp: dfa_trans_def dist_nodes_def) moreover from assms have "bdd_all (dfa_is_node M) (fst M ! p) ∧ bdd_all (dfa_is_node M) (fst M ! q)" by (simp add: wf_dfa_def dfa_is_node_def list_all_iff) moreover note assms(3,4) ultimately show "¬ check_eq (fst M ! q) (fst M ! p) T" by (auto simp: check_eq_dist_nodes) qed from assms have "tr_lookup (snd (iter M T)) q p = (if tr_lookup T q p then True else ¬ check_eq (fst M ! q) (fst M ! p) T)" by (auto simp add: iter_def wf_tr_def split_beta fold_map_idx_nth tr_lookup_def dfa_is_node_def) also have "… = (tr_lookup T q p ∨ ¬ check_eq (fst M ! q) (fst M ! p) T)" by simp also from assms C have "… = ((∃n<m. dist_nodes M n v p q) ∨ (∃n<m. dist_nodes M (Suc n) v p q))" by simp also have "… = (∃n < m. dist_nodes M n v p q ∨ dist_nodes M (Suc n) v p q)" by auto also have "… = (∃n < Suc m. dist_nodes M n v p q)" proof assume "∃n<m. dist_nodes M n v p q ∨ dist_nodes M (Suc n) v p q" then obtain n where D: "dist_nodes M n v p q ∨ dist_nodes M (Suc n) v p q" and N: "n < m" by blast moreover from N have "n < Suc m" by simp ultimately show "∃n < Suc m. dist_nodes M n v p q" by (elim disjE) blast+ next assume "∃n < Suc m. dist_nodes M n v p q" then obtain n where N: "n < Suc m" and D: "dist_nodes M n v p q" by blast from N have "n < m ∨ n = m" by auto from this D M' show "∃n<m. dist_nodes M n v p q ∨ dist_nodes M (Suc n) v p q" by auto qed finally show ?thesis by simp qed lemma fixpt_dist_nodes': assumes "wf_tr M T" and "wf_dfa M v" and "∀p q. dfa_is_node M q ∧ p < q ⟶ tr_lookup T q p = (∃n < m. dist_nodes M n v p q)" and "m > 0" and "dfa_is_node M q" and "p < q" shows "tr_lookup (fixpt M T) q p = (∃n. dist_nodes M n v p q)" using assms proof (induct M T arbitrary: m rule: fixpt_induct) case (1 M T m) let ?T = "snd (iter M T)" show ?case proof (cases "fst (iter M T)") case True { fix p' q' assume H: "dfa_is_node M q' ∧ p' < q'" with 1 have "tr_lookup ?T q' p' = (∃n < Suc m. dist_nodes M n v p' q')" by (simp only: iter_dist_nodes) } hence 2: "∀p q. dfa_is_node M q ∧ p < q ⟶ tr_lookup ?T q p = (∃n < Suc m. dist_nodes M n v p q)" by simp moreover from 1 have "wf_tr M ?T" by (simp add: iter_wf) moreover note 1(3,6,7) 1(1)[of "Suc m"] True ultimately have "tr_lookup (fixpt M ?T) q p = (∃n. dist_nodes M n v p q)" by simp with True show ?thesis by (simp add: Let_def split_beta) next case False then have F: "snd (iter M T) = T" by (simp add: iter_def fold_map_idx_fst_snd_eq split_beta) have C: "⋀m'. ∀p q. dfa_is_node M q ∧ p < q ⟶ tr_lookup T q p = (∃n < m' + m. dist_nodes M n v p q)" proof - fix m' show "∀p q. dfa_is_node M q ∧ p < q ⟶ tr_lookup T q p = (∃n < m' + m. dist_nodes M n v p q)" proof (induct m') case 0 with 1 show ?case by simp next case (Suc m') { fix p' q' assume H: "dfa_is_node M q'" and H2: "p' < q'" note 1(2,3) Suc moreover from Suc 1 have "0 < m' + m" by simp moreover note H H2 ultimately have "tr_lookup (snd (iter M T)) q' p' = (∃n < Suc (m' + m). dist_nodes M n v p' q')" by (rule iter_dist_nodes) with F have "tr_lookup T q' p' = (∃n < Suc m' + m. dist_nodes M n v p' q')" by simp } thus ?case by simp qed qed { fix p' q' assume H: "dfa_is_node M q' ∧ p' < q'" have "tr_lookup T q' p' = (∃n. dist_nodes M n v p' q')" proof assume "tr_lookup T q' p'" with H C[of 0] show "∃n. dist_nodes M n v p' q'" by auto next assume H': "∃n. dist_nodes M n v p' q'" then obtain n where "dist_nodes M n v p' q'" by blast moreover have "n < Suc n + m" by simp ultimately have "∃n' < Suc n + m. dist_nodes M n' v p' q'" by blast with H C[of "Suc n"] show "tr_lookup T q' p'" by simp qed } hence "∀p q. dfa_is_node M q ∧ p < q ⟶ tr_lookup T q p = (∃n. dist_nodes M n v p q)" by simp with False ‹dfa_is_node M q› ‹p < q› show ?thesis by simp qed qed lemma fixpt_dist_nodes: assumes "wf_dfa M v" and "dfa_is_node M p" and "dfa_is_node M q" shows "tr_lookup (fixpt M (init_tr M)) p q = (∃n. dist_nodes M n v p q)" proof - { fix p q assume H1: "p < q" and H2: "dfa_is_node M q" from init_tr_wf have "wf_tr M (init_tr M)" by simp moreover note assms(1) moreover { fix p' q' assume "dfa_is_node M q'" and "p' < q'" hence "tr_lookup (init_tr M) q' p' = dist_nodes M 0 v p' q'" by (rule init_tr_dist_nodes) also have "… = (∃n < 1. dist_nodes M n v p' q')" by auto finally have "tr_lookup (init_tr M) q' p' = (∃n<1. dist_nodes M n v p' q')" by simp } hence "∀p q. dfa_is_node M q ∧ p < q ⟶ tr_lookup (init_tr M) q p = (∃n<1. dist_nodes M n v p q)" by simp moreover note H1 H2 ultimately have "tr_lookup (fixpt M (init_tr M)) q p = (∃n. dist_nodes M n v p q)" by (simp only: fixpt_dist_nodes'[of _ _ _ 1]) } with assms(2,3) show ?thesis by (auto simp: tr_lookup_def dist_nodes_def) qed primrec mk_eqcl' :: "nat option list ⇒ nat ⇒ nat ⇒ nat ⇒ bool list list ⇒ nat option list" where "mk_eqcl' [] i j l T = []" | "mk_eqcl' (x#xs) i j l T = (if tr_lookup T j i ∨ x ≠ None then x else Some l) # mk_eqcl' xs i (Suc j) l T" lemma mk_eqcl'_len: "length (mk_eqcl' xs i j l T) = length xs" by (induct xs arbitrary: j) simp+ function mk_eqcl :: "nat option list ⇒ nat list ⇒ nat ⇒ bool list list ⇒ nat list × nat list" where "mk_eqcl [] zs i T = ([], zs)" | "mk_eqcl (None # xs) zs i T = (let (xs',zs') = mk_eqcl (mk_eqcl' xs i (Suc i) (length zs) T) (zs @ [i]) (Suc i) T in (length zs # xs', zs'))" | "mk_eqcl (Some l # xs) zs i T = (let (xs',zs') = mk_eqcl xs zs (Suc i) T in (l # xs', zs'))" by pat_completeness auto termination by (lexicographic_order simp: mk_eqcl'_len) lemma mk_eqcl'_bound: assumes "⋀x k. ⟦x ∈ set xs; x = Some k⟧ ⟹ k < l" and "x ∈ set (mk_eqcl' xs i j l T)" and "x = Some k" shows "k ≤ l" using assms proof (induct xs arbitrary: j) case (Cons y xs j) hence "x = y ∨ x = Some l ∨ x ∈ set (mk_eqcl' xs i (Suc j) l T)" by (cases "tr_lookup T j i ∨ y ≠ None") auto thus ?case proof (elim disjE) assume "x = y" hence "x ∈ set (y # xs)" by simp with Cons(2)[of x k] Cons(4) show ?thesis by simp qed (insert Cons, auto) qed simp lemma mk_eqcl'_nth': assumes "⋀x k. ⟦x ∈ set xs; x = Some k⟧ ⟹ k < l" and "⋀i'. ⟦i' < length xs; ¬ tr_lookup T (i' + j) i⟧ ⟹ xs ! i' = None" and "i < j" and "j' < length xs" shows "(mk_eqcl' xs i j l T ! j' = Some l) = (¬ tr_lookup T (j' + j) i)" using assms proof (induct xs arbitrary: j j') case (Cons x xs j) have I1:"⋀i'. ⟦i' < length xs; ¬ tr_lookup T (i' + Suc j) i⟧ ⟹ xs ! i' = None" proof - fix i' assume H: "i' < length xs" "¬ tr_lookup T (i' + Suc j) i" with Cons(3)[of "Suc i'"] show "xs ! i' = None" by simp qed have "j' = 0 ∨ j' > 0" by auto thus ?case proof (elim disjE) assume "j' > 0" then obtain j'' where J: "j' = Suc j''" by (cases j') simp+ from Cons(1)[of "Suc j" j''] I1 Cons(2,4,5) J show ?thesis by simp next assume H: "j' = 0" with Cons(3)[of 0] have "¬ tr_lookup T j i ⟹ x = None" by simp with Cons H show ?thesis by auto qed qed simp lemma mk_eqcl'_nth: assumes "⋀i' j' k. ⟦i' < length xs; j' < length xs; xs ! i' = Some k⟧ ⟹ (xs ! j' = Some k) = (¬ tr_lookup T (i' + jj) (j' + jj))" and "⋀a b c. ⟦a ≤ length T; b ≤ length T; c ≤ length T; ¬ tr_lookup T a b; ¬ tr_lookup T b c⟧ ⟹ ¬ tr_lookup T a c" and "length xs + jj = length T + 1" and "⋀x k. ⟦x ∈ set xs; x = Some k⟧ ⟹ k < l" and "⋀i'. ⟦i' < length xs; ¬ tr_lookup T (i' + jj) ii⟧ ⟹ xs ! i' = None" and "ii < jj" and "i < length xs" and "mk_eqcl' xs ii jj l T ! i = Some m" and "j < length xs" shows "(mk_eqcl' xs ii jj l T ! j = Some m) = (¬ tr_lookup T (i + jj) (j + jj))" using assms proof (induct xs arbitrary: jj i j) case Nil from Nil(7) have False by simp thus ?case by simp next case (Cons y xs jj i j) show ?case proof (cases i) case 0 show ?thesis proof (cases j) case 0 with ‹i=0› Cons(9) show ?thesis by (simp add: tr_lookup_def) next case (Suc j') from 0 Cons(5,9) have 1: "y = Some m ∧ m < l ∨ (y = None ∧ ¬ tr_lookup T jj ii ∧ m = l)" by (cases y, cases "tr_lookup T jj ii", auto) thus ?thesis proof (elim disjE) assume H: "y = Some m ∧ m < l" from Suc have "(mk_eqcl' (y # xs) ii jj l T ! j = Some m) = (mk_eqcl' xs ii (Suc jj) l T ! j' = Some m)" by simp also from H have "… = (xs ! j' = Some m)" proof (induct xs arbitrary: jj j') case (Cons a xs jj j') thus ?case by (cases j') simp+ qed simp also from Suc have "… = ((y # xs) ! j = Some m)" by simp also from Cons(2)[of i j m] Cons(8,10) Suc 0 H have "… = (¬ tr_lookup T (i + jj) (j + jj))" by simp finally show ?thesis by simp next assume H: "y = None ∧ ¬ tr_lookup T jj ii ∧ m = l" with Suc have "(mk_eqcl' (y # xs) ii jj l T ! j = Some m) = (mk_eqcl' xs ii (Suc jj) l T ! j' = Some l)" by simp also have "… = (¬ tr_lookup T (j' + Suc jj) ii)" proof (rule mk_eqcl'_nth') from Cons(5) show "⋀x k. ⟦x ∈ set xs; x = Some k⟧ ⟹ k < l" by simp show "⋀i'. ⟦i' < length xs; ¬ tr_lookup T (i' + Suc jj) ii⟧ ⟹ xs ! i' = None" proof - fix i' assume "i' < length xs" "¬ tr_lookup T (i' + Suc jj) ii" with Cons(6)[of "Suc i'"] show "xs ! i' = None" by simp qed from Cons(7) show "ii < Suc jj" by simp from Cons(10) Suc show "j' < length xs" by simp qed also from Suc H 0 have "… = (¬ tr_lookup T (j + jj) ii ∧ ¬ tr_lookup T (i + jj) ii)" by (simp add: add.commute) also have "… = (¬ tr_lookup T (i + jj) (j + jj) ∧ ¬ tr_lookup T (i + jj) ii)" proof assume H': "¬ tr_lookup T (j + jj) ii ∧ ¬ tr_lookup T (i + jj) ii" hence "¬ tr_lookup T ii (j + jj)" by (auto simp: tr_lookup_def) with H' Cons(3)[of "i + jj" ii "j + jj"] Cons(4,7,8,10) show "¬ tr_lookup T (i + jj) (j + jj) ∧ ¬ tr_lookup T (i + jj) ii" by simp next assume H': "¬ tr_lookup T (i + jj) (j + jj) ∧ ¬ tr_lookup T (i + jj) ii" hence "¬ tr_lookup T (j + jj) (i + jj)" by (auto simp: tr_lookup_def) with H' Cons(3)[of "j + jj" "i + jj" ii] Cons(4,7,8,10) show "¬ tr_lookup T (j + jj) ii ∧ ¬ tr_lookup T (i + jj) ii" by simp qed also from 0 H have "… = (¬ tr_lookup T (i + jj) (j + jj))" by simp finally show ?thesis by simp qed qed next case (Suc i') show ?thesis proof (cases j) case 0 have "m ≤ l" proof (rule mk_eqcl'_bound) from Cons(5) show "⋀x k. ⟦x ∈ set (y # xs); x = Some k⟧ ⟹ k < l" by simp from Cons(8) have "i < length (mk_eqcl' (y # xs) ii jj l T)" by (simp add: mk_eqcl'_len) with Cons(9) have "∃i < length (mk_eqcl' (y # xs) ii jj l T). mk_eqcl' (y # xs) ii jj l T ! i = Some m" by blast thus "Some m ∈ set (mk_eqcl' (y # xs) ii jj l T)" by (simp only: in_set_conv_nth) show "Some m = Some m" by simp qed hence "m < l ∨ m = l" by auto thus ?thesis proof (elim disjE) assume H: "m < l" with Cons(9) have I: "(y # xs) ! i = Some m" proof (induct ("y # xs") arbitrary: jj i) case (Cons a l jj i) thus ?case by (cases i) (auto, cases "tr_lookup T jj ii ∨ a ≠ None", simp+) qed simp from 0 H have "(mk_eqcl' (y # xs) ii jj l T ! j = Some m) = ((y#xs) ! j = Some m)" by (cases "tr_lookup T jj ii ∨ y ≠ None") simp+ also from Cons(8,10) I have "… = (¬ tr_lookup T (i + jj) (j + jj))" by (rule Cons(2)) finally show ?thesis by simp next assume H: "m = l" from Cons(5,6,7,8) have "(mk_eqcl' (y # xs) ii jj l T ! i = Some l) = (¬ tr_lookup T (i + jj) ii)" by (rule mk_eqcl'_nth') with H Cons(9) have I: "¬ tr_lookup T (i + jj) ii" by simp with 0 H Cons(5) have "(mk_eqcl' (y # xs) ii jj l T ! j = Some m) = (¬ tr_lookup T (j + jj) ii ∧ ¬ tr_lookup T (i + jj) ii ∧ y = None)" by auto also from Cons(6)[of 0] 0 have "… = (¬ tr_lookup T (j + jj) ii ∧ ¬ tr_lookup T (i + jj) ii)" by auto also have "… = (¬ tr_lookup T (i + jj) (j + jj) ∧ ¬ tr_lookup T (i + jj) ii)" proof assume H': "¬ tr_lookup T (j + jj) ii ∧ ¬ tr_lookup T (i + jj) ii" hence "¬ tr_lookup T ii (j + jj)" by (auto simp: tr_lookup_def) with H' Cons(3)[of "i + jj" ii "j + jj"] Cons(4,7,8,10) show "¬ tr_lookup T (i + jj) (j + jj) ∧ ¬ tr_lookup T (i + jj) ii" by simp next assume H': "¬ tr_lookup T (i + jj) (j + jj) ∧ ¬ tr_lookup T (i + jj) ii" hence "¬ tr_lookup T (j + jj) (i + jj)" by (auto simp: tr_lookup_def) with H' Cons(3)[of "j + jj" "i + jj" ii] Cons(4,7,8,10) show "¬ tr_lookup T (j + jj) ii ∧ ¬ tr_lookup T (i + jj) ii" by simp qed also from I have "… = (¬ tr_lookup T (i + jj) (j + jj))" by simp finally show ?thesis by simp qed next case (Suc j') hence "(mk_eqcl' (y # xs) ii jj l T ! j = Some m) = (mk_eqcl' xs ii (Suc jj) l T ! j' = Some m)" by simp also have "… = (¬ tr_lookup T (i' + Suc jj) (j' + Suc jj))" proof (rule Cons(1)) show "⋀i' j' k. ⟦i' < length xs; j' < length xs; xs ! i' = Some k⟧ ⟹ (xs ! j' = Some k) = (¬ tr_lookup T (i' + Suc jj) (j' + Suc jj))" proof - fix i' j' k assume "i' < length xs" "j' < length xs" "xs ! i' = Some k" with Cons(2)[of "Suc i'" "Suc j'" k] show "(xs ! j' = Some k) = (¬ tr_lookup T (i' + Suc jj) (j' + Suc jj))" by simp qed from Cons(3) show "⋀a b c. ⟦a ≤ length T; b ≤ length T; c ≤ length T; ¬ tr_lookup T a b; ¬ tr_lookup T b c ⟧ ⟹ ¬ tr_lookup T a c" by blast from Cons(4) show "length xs + Suc jj = length T + 1" by simp from Cons(5) show "⋀x k. ⟦x ∈ set xs; x = Some k⟧ ⟹ k < l" by simp show "⋀i'. ⟦i' < length xs; ¬ tr_lookup T (i' + Suc jj) ii⟧ ⟹ xs ! i' = None" proof - fix i' assume "i' < length xs" "¬ tr_lookup T (i' + Suc jj) ii" with Cons(6)[of "Suc i'"] show "xs ! i' = None" by simp qed from Cons(7) show "ii < Suc jj" by simp from Cons(8) ‹i=Suc i'› show "i' < length xs" by simp from Cons(9) ‹i=Suc i'› show "mk_eqcl' xs ii (Suc jj) l T ! i' = Some m" by simp from Cons(10) Suc show "j' < length xs" by simp qed also from Suc ‹i=Suc i'› have "… = (¬ tr_lookup T (i + jj) (j + jj))" by simp finally show ?thesis by simp qed qed qed lemma mk_eqcl'_Some: assumes "i < length xs" and "xs ! i ≠ None" shows "mk_eqcl' xs ii j l T ! i = xs ! i" using assms proof (induct xs arbitrary: j i) case (Cons y xs j i) thus ?case by (cases i) auto qed simp lemma mk_eqcl'_Some2: assumes "i < length xs" and "k < l" shows "(mk_eqcl' xs ii j l T ! i = Some k) = (xs ! i = Some k)" using assms proof (induct xs arbitrary: j i) case (Cons y xs j i) thus ?case by (cases i) auto qed simp lemma mk_eqcl_fst_Some: assumes "i < length xs" and "k < length zs" shows "(fst (mk_eqcl xs zs ii T) ! i = k) = (xs ! i = Some k)" using assms proof (induct xs zs ii T arbitrary: i rule: mk_eqcl.induct) case (2 xs zs ii T i) thus ?case by (cases i) (simp add: split_beta mk_eqcl'_len mk_eqcl'_Some2)+ next case (3 l xs zs ii T i) thus ?case by (cases i) (simp add: split_beta)+ qed simp lemma mk_eqcl_len_snd: "length zs ≤ length (snd (mk_eqcl xs zs i T))" by (induct xs zs i T rule: mk_eqcl.induct) (simp add: split_beta)+ lemma mk_eqcl_len_fst: "length (fst (mk_eqcl xs zs i T)) = length xs" by (induct xs zs i T rule: mk_eqcl.induct) (simp add: split_beta mk_eqcl'_len)+ lemma mk_eqcl_set_snd: assumes "i ∉ set zs" and "j > i" shows "i ∉ set (snd (mk_eqcl xs zs j T))" using assms by (induct xs zs j T rule: mk_eqcl.induct) (auto simp: split_beta) lemma mk_eqcl_snd_mon: assumes "⋀j1 j2. ⟦j1 < j2; j2 < length zs⟧ ⟹ zs ! j1 < zs ! j2" and "⋀x. x ∈ set zs ⟹ x < i" and "j1 < j2" and "j2 < length (snd (mk_eqcl xs zs i T))" shows "snd (mk_eqcl xs zs i T) ! j1 < snd (mk_eqcl xs zs i T) ! j2" using assms proof (induct xs zs i T rule: mk_eqcl.induct) case (2 xs zs i T) have "⋀j1 j2. ⟦j1 < j2; j2 < length (zs @ [i])⟧ ⟹ (zs @ [i]) ! j1 < (zs @ [i]) ! j2" proof - fix j1 j2 assume H: "j1 < j2" "j2 < length (zs @ [i])" hence "j2 < length zs ∨ j2 = length zs" by auto from this H 2 show "(zs @ [i]) ! j1 < (zs @ [i]) ! j2" by (elim disjE) (simp add: nth_append)+ qed moreover have "⋀x. x ∈ set (zs @ [i]) ⟹ x < Suc i" proof - fix x assume "x ∈ set (zs @ [i])" hence "x ∈ set zs ∨ x = i" by auto with 2(3)[of x] show "x < Suc i" by auto qed moreover note 2(4) moreover from 2(5) have "j2 < length (snd (mk_eqcl (mk_eqcl' xs i (Suc i) (length zs) T) (zs @ [i]) (Suc i) T))" by (simp add: split_beta) ultimately have "snd (mk_eqcl (mk_eqcl' xs i (Suc i) (length zs) T) (zs @ [i]) (Suc i) T) ! j1 < snd (mk_eqcl (mk_eqcl' xs i (Suc i) (length zs) T) (zs @ [i]) (Suc i) T) ! j2" by (rule 2(1)) thus ?case by (simp add: split_beta) next case (3 l xs zs i T) note 3(2) moreover have "⋀x. x ∈ set zs ⟹ x < Suc i" proof - fix x assume "x ∈ set zs" with 3(3)[of x] show "x < Suc i" by simp qed moreover note 3(4) moreover from 3(5) have "j2 < length (snd (mk_eqcl xs zs (Suc i) T))" by (simp add: split_beta) ultimately have "snd (mk_eqcl xs zs (Suc i) T) ! j1 < snd (mk_eqcl xs zs (Suc i) T) ! j2" by (rule 3(1)) thus ?case by (simp add: split_beta) qed simp lemma mk_eqcl_snd_nth: assumes "i < length zs" shows "snd (mk_eqcl xs zs j T) ! i = zs ! i" using assms by (induct xs zs j T rule: mk_eqcl.induct) (simp add: split_beta nth_append)+ lemma mk_eqcl_bound: assumes "⋀x k. ⟦x ∈ set xs; x = Some k⟧ ⟹ k < length zs" and "x ∈ set (fst (mk_eqcl xs zs ii T))" shows "x < length (snd (mk_eqcl xs zs ii T))" using assms proof (induct xs zs ii T rule: mk_eqcl.induct) case (2 xs zs i T) hence "x = length zs ∨ x ∈ set (fst (mk_eqcl (mk_eqcl' xs i (Suc i) (length zs) T) (zs @ [i]) (Suc i) T))" by (auto simp: split_beta) thus ?case proof (elim disjE) assume "x = length zs" hence "x < length (zs @ [i])" by simp also have "… ≤ length (snd (mk_eqcl (mk_eqcl' xs i (Suc i) (length zs) T) (zs @ [i]) (Suc i) T))" by (simp only: mk_eqcl_len_snd) finally show ?thesis by (simp add: split_beta) next assume H: "x ∈ set (fst (mk_eqcl (mk_eqcl' xs i (Suc i) (length zs) T) (zs @ [i]) (Suc i) T))" have "⋀x k. ⟦x ∈ set (mk_eqcl' xs i (Suc i) (length zs) T); x = Some k⟧ ⟹ k < length (zs @ [i])" proof - fix x k assume H': "x ∈ set (mk_eqcl' xs i (Suc i) (length zs) T)" " x = Some k" { fix x' k' assume "x' ∈ set xs" "x' = Some k'" with 2 have "k' < length zs" by simp } from this H' have "k ≤ length zs" by (rule mk_eqcl'_bound) thus "k < length (zs @ [i])" by simp qed with H 2 show ?thesis by (simp add: split_beta) qed next case (3 l xs zs i T) hence "x = l ∨ x ∈ set (fst (mk_eqcl xs zs (Suc i) T))" by (auto simp: split_beta) thus ?case proof (elim disjE) assume "x = l" with 3 have "x < length zs" by simp also from 3 have "… ≤ length (snd (mk_eqcl (Some l # xs) zs i T))" by (simp only: mk_eqcl_len_snd) finally show ?thesis by simp next assume "x ∈ set (fst (mk_eqcl xs zs (Suc i) T))" with 3 have "x < length (snd (mk_eqcl xs zs (Suc i) T))" by simp thus ?thesis by (simp add: split_beta) qed qed simp lemma mk_eqcl_fst_snd: assumes "⋀i. i < length zs ⟹ zs ! i < length xs + ii ∧ (zs ! i ≥ ii ⟶ xs ! (zs ! i - ii) = Some i)" and "⋀j1 j2. ⟦j1 < j2; j2 < length zs⟧ ⟹ zs ! j1 < zs ! j2" and "⋀z. z ∈ set zs ⟹ z < ii" and "i < length (snd (mk_eqcl xs zs ii T))" and "length xs + ii ≤ length T + 1" shows "snd (mk_eqcl xs zs ii T) ! i < length (fst (mk_eqcl xs zs ii T)) + ii ∧ (snd (mk_eqcl xs zs ii T) ! i ≥ ii ⟶ fst (mk_eqcl xs zs ii T) ! (snd (mk_eqcl xs zs ii T) ! i - ii) = i)" using assms proof (induct xs zs ii T arbitrary: i rule: mk_eqcl.induct) case (1 zs ii T i) from 1(1)[of i] 1(4,5) show ?case by simp next case (2 xs zs i T j) have "⋀i'. i' < length (zs @ [i]) ⟹ (zs @ [i]) ! i' < length (mk_eqcl' xs i (Suc i) (length zs) T) + Suc i ∧ (Suc i ≤ (zs @ [i]) ! i' ⟶ mk_eqcl' xs i (Suc i) (length zs) T ! ((zs @ [i]) ! i' - Suc i) = Some i')" proof - fix i' assume "i' < length (zs @ [i])" hence "i' < length zs ∨ i' = length zs" by auto thus "(zs @ [i]) ! i' < length (mk_eqcl' xs i (Suc i) (length zs) T) + Suc i ∧ (Suc i ≤ (zs @ [i]) ! i' ⟶ mk_eqcl' xs i (Suc i) (length zs) T ! ((zs @ [i]) ! i' - Suc i) = Some i')" proof (elim disjE) assume H: "i' < length zs" with 2(2) have I: "zs ! i' < length (None # xs) + i ∧ (i ≤ zs ! i' ⟶ (None # xs) ! (zs ! i' - i) = Some i')" by simp with H have G1: "(zs @ [i]) ! i' < length (mk_eqcl' xs i (Suc i) (length zs) T) + Suc i" by (auto simp: mk_eqcl'_len nth_append) { assume H': "Suc i ≤ (zs @ [i]) ! i'" then obtain k where K: "(zs @ [i]) ! i' - i = Suc k" by (cases "(zs @ [i]) ! i' - i") simp+ hence K': "k = (zs @ [i]) ! i' - Suc i" by simp from K H' H I have "xs ! k = Some i'" by (simp add: nth_append) with K I H have "mk_eqcl' xs i (Suc i) (length zs) T ! k = Some i'" by (auto simp add: mk_eqcl'_Some nth_append) with K' have "mk_eqcl' xs i (Suc i) (length zs) T ! ((zs @ [i]) ! i' - Suc i) = Some i'" by simp } with G1 show ?thesis by simp qed simp qed moreover have "⋀j1 j2. ⟦j1 < j2; j2 < length (zs @ [i])⟧ ⟹ (zs @ [i]) ! j1 < (zs @ [i]) ! j2" proof - fix j1 j2 assume H: "j1 < j2" "j2 < length (zs @ [i])" hence "j2 < length zs ∨ j2 = length zs" by auto from this H 2(3)[of j1 j2] 2(4)[of "zs ! j1"] show "(zs @ [i]) ! j1 < (zs @ [i]) ! j2" by (elim disjE) (simp add: nth_append)+ qed moreover have "⋀z. z ∈ set (zs @ [i]) ⟹ z < Suc i" proof - fix z assume "z ∈ set (zs @ [i])" hence "z ∈ set zs ∨ z = i" by auto with 2(4)[of z] show "z < Suc i" by auto qed moreover from 2 have "j < length (snd (mk_eqcl (mk_eqcl' xs i (Suc i) (length zs) T) (zs @ [i]) (Suc i) T))" by (simp add: split_beta) moreover from 2 have "length (mk_eqcl' xs i (Suc i) (length zs) T) + Suc i ≤ length T + 1" by (simp add: mk_eqcl'_len) ultimately have IV: "snd (mk_eqcl (mk_eqcl' xs i (Suc i) (length zs) T) (zs @ [i]) (Suc i) T) ! j < length (fst (mk_eqcl (mk_eqcl' xs i (Suc i) (length zs) T) (zs @ [i]) (Suc i) T)) + Suc i ∧ (Suc i ≤ snd (mk_eqcl (mk_eqcl' xs i (Suc i) (length zs) T) (zs @ [i]) (Suc i) T) ! j ⟶ fst (mk_eqcl (mk_eqcl' xs i (Suc i) (length zs) T) (zs @ [i]) (Suc i) T) ! (snd (mk_eqcl (mk_eqcl' xs i (Suc i) (length zs) T) (zs @ [i]) (Suc i) T) ! j - Suc i) = j)" by (rule 2(1)) hence G1: "snd (mk_eqcl (None # xs) zs i T) ! j < length (fst (mk_eqcl (None # xs) zs i T)) + i" by (auto simp: split_beta) { assume "i ≤ snd (mk_eqcl (None # xs) zs i T) ! j" hence "i = snd (mk_eqcl (None # xs) zs i T) ! j ∨ Suc i ≤ snd (mk_eqcl (None # xs) zs i T) ! j" by auto hence "fst (mk_eqcl (None # xs) zs i T) ! (snd (mk_eqcl (None # xs) zs i T) ! j - i) = j" proof (elim disjE) assume H: "i = snd (mk_eqcl (None # xs) zs i T) ! j" define k where "k = length zs" hence K: "snd (mk_eqcl (None # xs) zs i T) ! k = i" by (simp add: mk_eqcl_snd_nth split_beta) { assume "j ≠ k" hence "j < k ∨ j > k" by auto hence "snd (mk_eqcl (None # xs) zs i T) ! j ≠ i" proof (elim disjE) assume H': "j < k" from k_def have "k < length (zs @ [i])" by simp also have "… ≤ length (snd (mk_eqcl (mk_eqcl' xs i (Suc i) (length zs) T) (zs @ [i]) (Suc i) T))" by (simp only: mk_eqcl_len_snd) also have "… = length (snd (mk_eqcl (None # xs) zs i T))" by (simp add: split_beta) finally have K': "k < length (snd (mk_eqcl (None # xs) zs i T))" by simp from 2(3,4) H' this have "snd (mk_eqcl (None # xs) zs i T) ! j < snd (mk_eqcl (None # xs) zs i T) ! k" by (rule mk_eqcl_snd_mon) with K show ?thesis by simp next assume H': "j > k" from 2(3,4) H' 2(5) have "snd (mk_eqcl (None # xs) zs i T) ! k < snd (mk_eqcl (None # xs) zs i T) ! j" by (rule mk_eqcl_snd_mon) with K show ?thesis by simp qed } with H k_def have "j = length zs" by auto with H show ?thesis by (simp add: split_beta) next assume H: "Suc i ≤ snd (mk_eqcl (None # xs) zs i T) ! j" then obtain k where K: "snd (mk_eqcl (None # xs) zs i T) ! j - i = Suc k" by (cases "snd (mk_eqcl (None # xs) zs i T) ! j - i") simp+ hence K': "k = snd (mk_eqcl (None # xs) zs i T) ! j - Suc i" by simp from H IV have "fst (mk_eqcl (mk_eqcl' xs i (Suc i) (length zs) T) (zs @ [i]) (Suc i) T) ! (snd (mk_eqcl (mk_eqcl' xs i (Suc i) (length zs) T) (zs @ [i]) (Suc i) T) ! j - Suc i) = j" by (auto simp: split_beta) with K' have "fst (mk_eqcl (None # xs) zs i T) ! Suc k = j" by (simp add: split_beta) with K show ?thesis by simp qed } with G1 show ?case by simp next case (3 l xs zs i T j) have 1: "snd (mk_eqcl (Some l # xs) zs i T) = snd (mk_eqcl xs zs (Suc i) T)" by (simp add: split_beta) have 2: "length (fst (mk_eqcl (Some l # xs) zs i T)) = length (Some l # xs)" by (simp add: split_beta mk_eqcl_len_fst) have "⋀j. j < length zs ⟹ zs ! j < length xs + Suc i ∧ (Suc i ≤ zs ! j ⟶ xs ! (zs ! j - Suc i) = Some j)" proof - fix j assume H: "j < length zs" with 3(2)[of j] have I: "zs ! j < length (Some l # xs) + i ∧ (i ≤ zs ! j ⟶ (Some l # xs) ! (zs ! j - i) = Some j)" by simp hence G1: "zs ! j < length xs + Suc i" and G2: "i ≤ zs ! j ⟶ (Some l # xs) ! (zs ! j - i) = Some j" by simp+ { assume H2: "Suc i ≤ zs ! j" then obtain k where K: "zs ! j - i = Suc k" by (cases "zs ! j - i") simp+ with H2 G2 have "xs ! k = Some j" by simp moreover from K have "k = zs ! j - Suc i" by simp ultimately have "xs ! (zs ! j - Suc i) = Some j" by simp } with G1 show "zs ! j < length xs + Suc i ∧ (Suc i ≤ zs ! j ⟶ xs ! (zs ! j - Suc i) = Some j)" by simp qed moreover note 3(3) moreover have "⋀z. z ∈ set zs ⟹ z < Suc i" proof - fix z assume "z ∈ set zs" with 3(4)[of z] show "z < Suc i" by simp qed moreover from 3(5) 1 have "j < length (snd (mk_eqcl xs zs (Suc i) T))" by simp moreover from 3 have "length xs + Suc i ≤ length T + 1" by simp ultimately have IV: "snd (mk_eqcl xs zs (Suc i) T) ! j < length (fst (mk_eqcl xs zs (Suc i) T)) + Suc i ∧ (Suc i ≤ snd (mk_eqcl xs zs (Suc i) T) ! j ⟶ fst (mk_eqcl xs zs (Suc i) T) ! (snd (mk_eqcl xs zs (Suc i) T) ! j - Suc i) = j)" by (rule 3(1)) with 1 have G1: "snd (mk_eqcl (Some l # xs) zs i T) ! j < length (fst (mk_eqcl (Some l # xs) zs i T)) + i" by (simp add: split_beta mk_eqcl_len_fst) { assume "i ≤ snd (mk_eqcl (Some l # xs) zs i T) ! j" hence "i = snd (mk_eqcl (Some l # xs) zs i T) ! j ∨ i < snd (mk_eqcl (Some l # xs) zs i T) ! j" by auto hence "fst (mk_eqcl (Some l # xs) zs i T) ! (snd (mk_eqcl (Some l # xs) zs i T) ! j - i) = j" proof (elim disjE) assume H: "i = snd (mk_eqcl (Some l # xs) zs i T) ! j" with 3 1 have "∃j < length (snd (mk_eqcl xs zs (Suc i) T)). snd (mk_eqcl xs zs (Suc i) T) ! j = i" by auto hence T1: "i ∈ set (snd (mk_eqcl xs zs (Suc i) T))" by (simp only: in_set_conv_nth) from 3(4) have "i ∉ set zs" by auto hence "i ∉ set (snd (mk_eqcl xs zs (Suc i) T))" by (simp add: mk_eqcl_set_snd) with T1 show ?thesis by simp next assume H: "i < snd (mk_eqcl (Some l # xs) zs i T) ! j" from H obtain k where K: "snd (mk_eqcl (Some l # xs) zs i T) ! j - i = Suc k" by (cases "snd (mk_eqcl (Some l # xs) zs i T) ! j - i") simp+ hence K': "snd (mk_eqcl (Some l # xs) zs i T) ! j - Suc i = k" by simp from 1 H IV have "fst (mk_eqcl xs zs (Suc i) T) ! (snd (mk_eqcl xs zs (Suc i) T) ! j - Suc i) = j" by simp with K K' show ?thesis by (simp add: split_beta) qed } with G1 show ?case by simp qed lemma mk_eqcl_fst_nth: assumes "⋀i j k. ⟦i < length xs; j < length xs; xs ! i = Some k⟧ ⟹ (xs ! j = Some k) = (¬ tr_lookup T (i + ii) (j + ii))" and "⋀a b c. ⟦a ≤ length T; b ≤ length T; c ≤ length T; ¬ tr_lookup T a b; ¬ tr_lookup T b c⟧ ⟹ ¬ tr_lookup T a c" and "⋀x k. ⟦x ∈ set xs; x = Some k⟧ ⟹ k < length zs" and "length xs + ii = length T + 1" and "i < length xs" and "j < length xs" shows "(fst (mk_eqcl xs zs ii T) ! i = fst (mk_eqcl xs zs ii T) ! j) = (¬ tr_lookup T (i + ii) (j + ii))" using assms proof (induct xs zs ii T arbitrary: i j rule: mk_eqcl.induct) case (1 zs ii T) thus ?case by simp next case (2 xs zs ii T) { fix i j assume H: "i < j" "j < length (None # xs)" then obtain j' where J: "j = Suc j'" by (cases j) simp+ have "(fst (mk_eqcl (None # xs) zs ii T) ! i = fst (mk_eqcl (None # xs) zs ii T) ! j) = (¬ tr_lookup T (i + ii) (j + ii))" proof (cases i) case 0 with J have "(fst (mk_eqcl (None # xs) zs ii T) ! i = fst (mk_eqcl (None # xs) zs ii T) ! j) = (fst (mk_eqcl (mk_eqcl' xs ii (Suc ii) (length zs) T) (zs @ [ii]) (Suc ii) T) ! j' = length zs)" by (auto simp add: split_beta) also from H J have "… = (mk_eqcl' xs ii (Suc ii) (length zs) T ! j' = Some (length zs))" by (simp add: mk_eqcl_fst_Some mk_eqcl'_len) also have "… = (¬ tr_lookup T (j' + Suc ii) ii)" proof - have "⋀x k. ⟦x ∈ set xs; x = Some k⟧ ⟹ k < length zs" proof - fix x k assume "x ∈ set xs" "x = Some k" with 2(4)[of x k] show "k < length zs" by simp qed moreover have "⋀i'. ⟦i' < length xs; ¬ tr_lookup T (i' + Suc ii) ii⟧ ⟹ xs ! i' = None" proof - fix i' assume H: "i' < length xs" "¬ tr_lookup T (i' + Suc ii) ii" { assume H': "xs ! i' ≠ None" then obtain k where "xs ! i' = Some k" by (cases "xs ! i'") simp+ with 2(2)[of "Suc i'" 0 k] H have False by simp } thus "xs ! i' = None" by (cases "xs ! i'") simp+ qed moreover from H J have "ii < Suc ii" "j' < length xs" by simp+ ultimately show ?thesis by (rule mk_eqcl'_nth') qed also from J 0 have "… = (¬ tr_lookup T (i + ii) (j + ii))" by (auto simp: tr_lookup_def) finally show ?thesis by simp next case (Suc i') have "⋀i j k. ⟦i < length (mk_eqcl' xs ii (Suc ii) (length zs) T); j < length (mk_eqcl' xs ii (Suc ii) (length zs) T); mk_eqcl' xs ii (Suc ii) (length zs) T ! i = Some k⟧ ⟹ (mk_eqcl' xs ii (Suc ii) (length zs) T ! j = Some k) = (¬ tr_lookup T (i + Suc ii) (j + Suc ii))" proof - fix i j k assume H: "i < length (mk_eqcl' xs ii (Suc ii) (length zs) T)" "j < length (mk_eqcl' xs ii (Suc ii) (length zs) T)" "mk_eqcl' xs ii (Suc ii) (length zs) T ! i = Some k" { fix i' j' k assume "i' < length xs" "j' < length xs" "xs ! i' = Some k" with 2(2)[of "Suc i'" "Suc j'" k] have "(xs ! j' = Some k) = (¬ tr_lookup T (i' + Suc ii) (j' + Suc ii))" by simp } moreover note 2(3) moreover from 2(5) have "length xs + Suc ii = length T + 1" by simp moreover { fix x k assume "x ∈ set xs" "x = Some k" with 2(4)[of x k] have "k < length zs" by simp } moreover have "⋀i'. ⟦i' < length xs; ¬ tr_lookup T (i' + Suc ii) ii⟧ ⟹ xs ! i' = None" proof - fix i' assume H': "i' < length xs" "¬ tr_lookup T (i' + Suc ii) ii" { assume "xs ! i' ≠ None" then obtain k where K: "xs ! i' = Some k" by (cases "xs ! i'") simp+ with H' 2(2)[of "Suc i'" 0 k] have False by simp } thus "xs ! i' = None" by (cases "xs ! i' = None") simp+ qed moreover have "ii < Suc ii" by simp moreover from H have "i < length xs" by (simp add: mk_eqcl'_len) moreover note H(3) moreover from H have "j < length xs" by (simp add: mk_eqcl'_len) ultimately show "(mk_eqcl' xs ii (Suc ii) (length zs) T ! j = Some k) = (¬ tr_lookup T (i + Suc ii) (j + Suc ii))" by (rule mk_eqcl'_nth) qed moreover note 2(3) moreover have "⋀x k. ⟦x ∈ set (mk_eqcl' xs ii (Suc ii) (length zs) T); x = Some k⟧ ⟹ k < length (zs @ [ii])" proof - fix x k assume H: "x ∈ set (mk_eqcl' xs ii (Suc ii) (length zs) T)" "x = Some k" { fix x k assume "x ∈ set xs" "x = Some k" with 2(4)[of x k] have "k < length zs" by simp } from this H have "k ≤ length zs" by (rule mk_eqcl'_bound) thus "k < length (zs @ [ii])" by simp qed moreover from 2(5) have "length (mk_eqcl' xs ii (Suc ii) (length zs) T) + Suc ii = length T + 1" by (simp add: mk_eqcl'_len) moreover from H Suc J have "i' < length (mk_eqcl' xs ii (Suc ii) (length zs) T)" "j' < length (mk_eqcl' xs ii (Suc ii) (length zs) T)" by (simp add: mk_eqcl'_len)+ ultimately have IV: "(fst (mk_eqcl (mk_eqcl' xs ii (Suc ii) (length zs) T) (zs @ [ii]) (Suc ii) T) ! i' = fst (mk_eqcl (mk_eqcl' xs ii (Suc ii) (length zs) T) (zs @ [ii]) (Suc ii) T) ! j') = (¬ tr_lookup T (i' + Suc ii) (j' + Suc ii))" by (rule 2(1)) with Suc J show ?thesis by (simp add: split_beta) qed } note L = this have "i < j ∨ i = j ∨ i > j" by auto thus ?case proof (elim disjE) assume "i > j" with 2(6) L have "(fst (mk_eqcl (None # xs) zs ii T) ! j = fst (mk_eqcl (None # xs) zs ii T) ! i) = (¬ tr_lookup T (i + ii) (j + ii))" by (auto simp: tr_lookup_def) thus ?thesis by auto qed (insert 2(7) L, simp add: tr_lookup_def)+ next case (3 l xs zs ii T i j) { fix i j assume H: "i < j" "j < length (Some l # xs)" then obtain j' where J: "j = Suc j'" by (cases j) simp+ have "(fst (mk_eqcl (Some l # xs) zs ii T) ! i = fst (mk_eqcl (Some l # xs) zs ii T) ! j) = (¬ tr_lookup T (i + ii) (j + ii))" proof (cases i) case 0 with J have "(fst (mk_eqcl (Some l # xs) zs ii T) ! i = fst (mk_eqcl (Some l # xs) zs ii T) ! j) = (fst (mk_eqcl xs zs (Suc ii) T) ! j' = l)" by (auto simp add: split_beta) also from 3(4)[of "Some l" l] H J have "… = (xs ! j' = Some l)" by (simp add: mk_eqcl_fst_Some) also from J have "… = ((Some l # xs) ! j = Some l)" by simp also from H 0 3(2)[of i j l] have "… = (¬ tr_lookup T (i + ii) (j + ii))" by simp finally show ?thesis by simp next case (Suc i') have "⋀i j k. ⟦i < length xs; j < length xs; xs ! i = Some k⟧ ⟹ (xs ! j = Some k) = (¬ tr_lookup T (i + Suc ii) (j + Suc ii))" proof - fix i j k assume "i < length xs" "j < length xs" "xs ! i = Some k" with 3(2)[of "Suc i" "Suc j" k] show "(xs ! j = Some k) = (¬ tr_lookup T (i + Suc ii) (j + Suc ii))" by simp qed moreover note 3(3) moreover have "⋀x k. ⟦x ∈ set xs; x = Some k⟧ ⟹ k < length zs" proof - fix x k assume "x ∈ set xs" "x = Some k" with 3(4)[of x k] show "k < length zs" by simp qed moreover from 3(5) H Suc J have "length xs + Suc ii = length T + 1" "i' < length xs" "j' < length xs" by simp+ ultimately have "(fst (mk_eqcl xs zs (Suc ii) T) ! i' = fst (mk_eqcl xs zs (Suc ii) T) ! j') = (¬ tr_lookup T (i' + Suc ii) (j' + Suc ii))" by (rule 3(1)) with J Suc show ?thesis by (simp add: split_beta) qed } note L = this have "i < j ∨ i = j ∨ i > j" by auto thus ?case proof (elim disjE) assume "i > j" with 3(6) L have "(fst (mk_eqcl (Some l # xs) zs ii T) ! j = fst (mk_eqcl (Some l # xs) zs ii T) ! i) = (¬ tr_lookup T (j + ii) (i + ii))" by simp thus ?thesis by (auto simp: tr_lookup_def) qed (insert 3(7) L, simp add: tr_lookup_def)+ qed definition min_dfa :: "dfa ⇒ dfa" where "min_dfa = (λ(bd, as). let (os, ns) = mk_eqcl (replicate (length bd) None) [] 0 (fixpt (bd, as) (init_tr (bd, as))) in (map (λp. bdd_map (λq. os ! q) (bd ! p)) ns, map (λp. as ! p) ns))" definition eq_nodes :: "dfa ⇒ nat ⇒ nat ⇒ nat ⇒ bool" where "eq_nodes = (λM v p q. ¬ (∃n. dist_nodes M n v p q))" lemma mk_eqcl_fixpt_fst_bound: assumes "dfa_is_node M i" shows "fst (mk_eqcl (replicate (length (fst M)) None) [] 0 (fixpt M (init_tr M))) ! i < length (snd (mk_eqcl (replicate (length (fst M)) None) [] 0 (fixpt M (init_tr M))))" (is "fst ?M ! i < length (snd ?M)") proof - { fix x k assume H: "x ∈ set (replicate (length (fst M)) (None::nat option))" "x = Some k" hence "k < length []" by (cases "length (fst M) = 0") simp+ } moreover from assms have "fst ?M ! i ∈ set (fst ?M)" by (simp add: dfa_is_node_def mk_eqcl_len_fst) ultimately show ?thesis by (rule mk_eqcl_bound) qed lemma mk_eqcl_fixpt_fst_nth: assumes "wf_dfa M v" and "dfa_is_node M p" and "dfa_is_node M q" shows "(fst (mk_eqcl (replicate (length (fst M)) None) [] 0 (fixpt M (init_tr M))) ! p = fst (mk_eqcl (replicate (length (fst M)) None) [] 0 (fixpt M (init_tr M))) ! q) = eq_nodes M v p q" (is "(fst ?M ! p = fst ?M ! q) = eq_nodes M v p q") proof - have WF: "wf_tr M (fixpt M (init_tr M))" by (simp only: fixpt_wf init_tr_wf) have "(fst ?M ! p = fst ?M ! q) = (¬ tr_lookup (fixpt M (init_tr M)) p q)" proof - { fix i j k assume H: "i < length (replicate (length (fst M)) None)" "j < length (replicate (length (fst M)) None)" "replicate (length (fst M)) None ! i = Some k" hence "(replicate (length (fst M)) None ! j = Some k) = (¬ tr_lookup (fixpt M (init_tr M)) (i + 0) (j + 0))" by simp } moreover have "⋀a b c. ⟦a ≤ length (fixpt M (init_tr M)); b ≤ length (fixpt M (init_tr M)); c ≤ length (fixpt M (init_tr M)); ¬ tr_lookup (fixpt M (init_tr M)) a b; ¬ tr_lookup (fixpt M (init_tr M)) b c⟧ ⟹ ¬ tr_lookup (fixpt M (init_tr M)) a c" proof - fix a b c assume H': "a ≤ length (fixpt M (init_tr M))" "b ≤ length (fixpt M (init_tr M))" "c ≤ length (fixpt M (init_tr M))" "¬ tr_lookup (fixpt M (init_tr M)) a b" "¬ tr_lookup (fixpt M (init_tr M)) b c" { fix q assume H'': "q ≤ length (fixpt M (init_tr M))" from assms have "length (fst M) > 0" by (simp add: wf_dfa_def) then obtain m where M: "length (fst M) = Suc m" by (cases "length (fst M)") simp+ hence M': "m = length (fst M) - 1" by simp with H'' WF have "q ≤ m" by (simp add: wf_tr_def) with M have "q < length (fst M)" by simp } with H' have D: "dfa_is_node M a" "dfa_is_node M b" "dfa_is_node M c" by (auto simp: dfa_is_node_def) with H'(4,5) assms(1) have "¬ (∃n. dist_nodes M n v a b)" "¬ (∃n. dist_nodes M n v b c)" by (simp add: fixpt_dist_nodes[symmetric])+ hence "¬ (∃n. dist_nodes M n v a c)" by (auto simp: dist_nodes_def) with H' assms D show "¬ tr_lookup (fixpt M (init_tr M)) a c" by (simp add: fixpt_dist_nodes[symmetric]) qed moreover have "⋀x k. ⟦x ∈ set (replicate (length (fst M)) None); x = Some k⟧ ⟹ k < length []" proof - fix x k assume "x ∈ set (replicate (length (fst M)) (None::nat option))" "x = Some k" thus "k < length []" by (cases "length (fst M) = 0") simp+ qed moreover from WF assms have "length (replicate (length (fst M)) None) + 0 = length (fixpt M (init_tr M)) + 1" by (simp add: wf_tr_def wf_dfa_def) moreover from assms have "p < length (replicate (length (fst M)) None)" "q < length (replicate (length (fst M)) None)" by (simp add: dfa_is_node_def)+ ultimately have "(fst ?M ! p = fst ?M ! q) = (¬ tr_lookup (fixpt M (init_tr M)) (p+0) (q+0))" by (rule mk_eqcl_fst_nth) thus ?thesis by simp qed also from assms have "… = eq_nodes M v p q" by (simp only: fixpt_dist_nodes eq_nodes_def) finally show ?thesis by simp qed lemma mk_eqcl_fixpt_fst_snd_nth: assumes "i < length (snd (mk_eqcl (replicate (length (fst M)) None) [] 0 (fixpt M (init_tr M))))" and "wf_dfa M v" shows "snd (mk_eqcl (replicate (length (fst M)) None) [] 0 (fixpt M (init_tr M))) ! i < length (fst (mk_eqcl (replicate (length (fst M)) None) [] 0 (fixpt M (init_tr M)))) ∧ fst (mk_eqcl (replicate (length (fst M)) None) [] 0 (fixpt M (init_tr M))) ! (snd (mk_eqcl (replicate (length (fst M)) None) [] 0 (fixpt M (init_tr M))) ! i) = i" (is "snd ?M ! i < length (fst ?M) ∧ fst ?M ! (snd ?M ! i) = i") proof - have "⋀i. i < length [] ⟹ [] ! i < length (replicate (length (fst M)) None) + 0 ∧ (0 ≤ [] ! i ⟶ replicate (length (fst M)) None ! ([] ! i - 0) = Some i)" by simp moreover have "⋀j1 j2. ⟦j1 < j2; j2 < length []⟧ ⟹ [] ! j1 < [] ! j2" by simp moreover have "⋀z. z ∈ set [] ⟹ z < 0" by simp moreover note assms(1) moreover have "length (replicate (length (fst M)) None) + 0 ≤ length (fixpt M (init_tr M)) + 1" proof - have WF: "wf_tr M (fixpt M (init_tr M))" by (simp only: init_tr_wf fixpt_wf) from assms have "length (fst M) > 0" by (simp add: wf_dfa_def) then obtain m where M:"length (fst M) = Suc m" by (cases "length (fst M)") simp+ hence M': "m = length (fst M) - 1" by simp with WF have "length (fixpt M (init_tr M)) = m" by (simp add: wf_tr_def) with M show ?thesis by simp qed ultimately have "snd ?M ! i < length (fst ?M) + 0 ∧ (0 ≤ snd ?M ! i ⟶ fst ?M ! (snd ?M ! i - 0) = i)" by (rule mk_eqcl_fst_snd) thus ?thesis by simp qed lemma eq_nodes_dfa_trans: assumes "eq_nodes M v p q" and "is_alph v bs" shows "eq_nodes M v (dfa_trans M p bs) (dfa_trans M q bs)" proof (rule ccontr) assume H: "¬ eq_nodes M v (dfa_trans M p bs) (dfa_trans M q bs)" then obtain n w where "length w = n" "list_all (is_alph v) w" "dfa_accepting M (dfa_steps M (dfa_trans M p bs) w) ≠ dfa_accepting M (dfa_steps M (dfa_trans M q bs) w)" unfolding eq_nodes_def dist_nodes_def by blast with assms have "length (bs # w) = Suc n" "list_all (is_alph v) (bs # w)" "dfa_accepting M (dfa_steps M p (bs # w)) ≠ dfa_accepting M (dfa_steps M q (bs # w))" by simp+ hence "¬ eq_nodes M v p q" unfolding eq_nodes_def dist_nodes_def by blast with assms show False by simp qed lemma mk_eqcl_fixpt_trans: assumes "wf_dfa M v" and "dfa_is_node M p" and "is_alph v bs" shows "dfa_trans (min_dfa M) (fst (mk_eqcl (replicate (length (fst M)) None) [] 0 (fixpt M (init_tr M))) ! p) bs = fst (mk_eqcl (replicate (length (fst M)) None) [] 0 (fixpt M (init_tr M))) ! (dfa_trans M p bs)" (is "dfa_trans (min_dfa M) (fst ?M ! p) bs = fst ?M ! (dfa_trans M p bs)") proof - let ?q = "snd ?M ! (fst ?M ! p)" from assms have I1: "?q < length (fst ?M)" "fst ?M ! ?q = fst ?M ! p" by (simp add: mk_eqcl_fixpt_fst_bound mk_eqcl_fixpt_fst_snd_nth)+ with assms have I2: "bddh (length bs) (fst M ! ?q)" by (simp add: mk_eqcl_len_fst wf_dfa_def list_all_iff is_alph_def) from I1 have I3: "dfa_is_node M ?q" by (simp add: mk_eqcl_len_fst dfa_is_node_def) with assms I1 have "eq_nodes M v p ?q" by (simp add: mk_eqcl_fixpt_fst_nth[symmetric]) with assms have "eq_nodes M v (dfa_trans M p bs) (dfa_trans M ?q bs)" by (simp add: eq_nodes_dfa_trans) with assms I3 have "fst ?M ! (dfa_trans M p bs) = fst ?M ! (dfa_trans M ?q bs)" by (simp add: dfa_trans_is_node mk_eqcl_fixpt_fst_nth) with assms I2 show ?thesis by (simp add: dfa_trans_def min_dfa_def split_beta mk_eqcl_fixpt_fst_bound bdd_map_bdd_lookup) qed lemma mk_eqcl_fixpt_steps: assumes "wf_dfa M v" and "dfa_is_node M p" and "list_all (is_alph v) w" shows "dfa_steps (min_dfa M) (fst (mk_eqcl (replicate (length (fst M)) None) [] 0 (fixpt M (init_tr M))) ! p) w = fst (mk_eqcl (replicate (length (fst M)) None) [] 0 (fixpt M (init_tr M))) ! (dfa_steps M p w)" (is "dfa_steps (min_dfa M) (fst ?M ! p) w = fst ?M ! (dfa_steps M p w)") using assms by (induct w arbitrary: p) (simp add: mk_eqcl_fixpt_trans dfa_trans_is_node)+ lemma mk_eqcl_fixpt_startnode: assumes "length (fst M) > 0" shows "length (snd (mk_eqcl (replicate (length (fst M)) None) [] 0 (fixpt M (init_tr M)))) > 0 ∧ fst (mk_eqcl (replicate (length (fst M)) None) [] 0 (fixpt M (init_tr M))) ! 0 = 0 ∧ snd (mk_eqcl (replicate (length (fst M)) None) [] 0 (fixpt M (init_tr M))) ! 0 = 0" (is "length (snd ?M) > 0 ∧ fst ?M ! 0 = 0 ∧ snd ?M ! 0 = 0") proof - from assms obtain k where K: "length (fst M) = Suc k" by (cases "length (fst M)") simp+ from K have "length (snd ?M) = length (snd (mk_eqcl (mk_eqcl' (replicate k None) 0 (Suc 0) 0 (fixpt M (init_tr M))) [0] (Suc 0) (fixpt M (init_tr M))))" by (simp add: split_beta) also have "… ≥ length [0::nat]" by (simp only: mk_eqcl_len_snd) finally have "length (snd ?M) > 0" by auto with K show ?thesis by (simp add: split_beta mk_eqcl_snd_nth) qed lemma min_dfa_wf: "wf_dfa M v ⟹ wf_dfa (min_dfa M) v" proof - assume H: "wf_dfa M v" obtain bd as where "min_dfa M = (bd, as)" by (cases "min_dfa M") auto hence M: "bd = fst (min_dfa M)" "as = snd (min_dfa M)" by simp+ let ?M = "mk_eqcl (replicate (length (fst M)) None) [] 0 (fixpt M (init_tr M))" { fix x assume "x ∈ set bd" then obtain i where I: "i < length bd" "x = bd ! i" by (auto simp: in_set_conv_nth) with M H have "snd ?M ! i < length (fst ?M)" by (simp add: min_dfa_def split_beta mk_eqcl_fixpt_fst_snd_nth) hence N: "dfa_is_node M (snd ?M ! i)" by (simp add: mk_eqcl_len_fst dfa_is_node_def) with H have BH: "bddh v (fst M ! (snd ?M ! i))" by (simp add: wf_dfa_def list_all_iff dfa_is_node_def) from I M have BI: "bd ! i = bdd_map (λq. fst ?M ! q) (fst M ! (snd ?M ! i))" by (simp add: split_beta min_dfa_def) with BH have G1: "bddh v (bd ! i)" by (simp add: bddh_bdd_map) from H N have "bdd_all (dfa_is_node M) (fst M ! (snd ?M ! i))" by (simp add: wf_dfa_def list_all_iff dfa_is_node_def) moreover { fix q assume "dfa_is_node M q" hence "fst ?M ! q < length (snd ?M)" by (simp add: mk_eqcl_fixpt_fst_bound) hence "dfa_is_node (min_dfa M) (fst ?M ! q)" by (simp add: dfa_is_node_def min_dfa_def split_beta) } ultimately have "bdd_all (dfa_is_node (min_dfa M)) (bdd_map (λq. fst ?M ! q) (fst M ! (snd ?M ! i)))" by (simp add: bdd_all_bdd_map) with G1 BI I have "bddh v x ∧ bdd_all (dfa_is_node (min_dfa M)) x" by simp } hence G: "list_all (bddh v) bd ∧ list_all (bdd_all (dfa_is_node (min_dfa M))) bd" by (simp add: list_all_iff) from H have "length (fst M) > 0" by (simp add: wf_dfa_def) hence "length (snd ?M) > 0" by (auto simp only: mk_eqcl_fixpt_startnode) with G M show "wf_dfa (min_dfa M) v" by (simp add: wf_dfa_def min_dfa_def split_beta) qed lemma min_dfa_accept: assumes "wf_dfa M v" and "list_all (is_alph v) w" shows "dfa_accepts (min_dfa M) w = dfa_accepts M w" proof - let ?M = "mk_eqcl (replicate (length (fst M)) None) [] 0 (fixpt M (init_tr M))" from assms have "length (fst M) > 0" by (simp add: wf_dfa_def) hence SN: "length (snd ?M) > 0 ∧ fst ?M ! 0 = 0 ∧ snd ?M ! 0 = 0" by (auto simp only: mk_eqcl_fixpt_startnode) have D: "dfa_steps (min_dfa M) 0 w = fst ?M ! dfa_steps M 0 w" proof - from assms have "dfa_is_node M 0" by (simp add: wf_dfa_def dfa_is_node_def) moreover from SN have "dfa_steps (min_dfa M) 0 w = dfa_steps (min_dfa M) (fst ?M ! 0) w" by simp moreover note assms ultimately show ?thesis by (simp add: mk_eqcl_fixpt_steps) qed from assms have WF: "wf_dfa (min_dfa M) v" by (simp add: min_dfa_wf) hence "dfa_is_node (min_dfa M) 0" by (simp add: dfa_startnode_is_node) with WF assms have "dfa_is_node (min_dfa M) (dfa_steps (min_dfa M) 0 w)" by (simp add: dfa_steps_is_node) with D have DN: "dfa_is_node (min_dfa M) (fst ?M ! dfa_steps M 0 w)" by simp let ?q = "snd ?M ! (fst ?M ! dfa_steps M 0 w)" from assms have N: "dfa_is_node M (dfa_steps M 0 w)" by (simp add: dfa_steps_is_node dfa_startnode_is_node) with assms have I: "?q < length (fst ?M)" "fst ?M ! ?q = fst ?M ! dfa_steps M 0 w" by (simp add: mk_eqcl_fixpt_fst_bound mk_eqcl_fixpt_fst_snd_nth)+ hence "dfa_is_node M ?q" by (simp add: mk_eqcl_len_fst dfa_is_node_def) with assms N I have EQ: "eq_nodes M v (dfa_steps M 0 w) ?q" by (simp add: mk_eqcl_fixpt_fst_nth[symmetric]) have A: "dfa_accepting M (dfa_steps M 0 w) = dfa_accepting M ?q" proof (rule ccontr) assume H: "dfa_accepting M (dfa_steps M 0 w) ≠ dfa_accepting M ?q" hence "dist_nodes M 0 v (dfa_steps M 0 w) ?q" by (auto simp: dist_nodes_def) with EQ show False by (simp add: eq_nodes_def) qed from D have "dfa_accepts (min_dfa M) w = snd (min_dfa M) ! (fst ?M ! dfa_steps M 0 w)" by (simp add: accepts_def dfa_accepting_def) also from WF DN have "… = dfa_accepting M ?q" by (simp add: dfa_is_node_def wf_dfa_def min_dfa_def split_beta dfa_accepting_def) also from A have "… = dfa_accepts M w" by (simp add: accepts_def) finally show ?thesis by simp qed section ‹NFAs› type_synonym nbddtable = "bool list bdd list" type_synonym nfa = "nbddtable × astate" definition nfa_is_node :: "nfa ⇒ bool list ⇒ bool" where "nfa_is_node A = (λqs. length qs = length (fst A))" definition wf_nfa :: "nfa ⇒ nat ⇒ bool" where "wf_nfa A n = (list_all (bddh n) (fst A) ∧ list_all (bdd_all (nfa_is_node A)) (fst A) ∧ length (snd A) = length (fst A) ∧ length (fst A) > 0)" definition set_of_bv :: "bool list ⇒ nat set" where "set_of_bv bs = {i. i < length bs ∧ bs ! i}" fun bv_or :: "bool list ⇒ bool list ⇒ bool list" where "bv_or [] [] = []" | "bv_or (x # xs) (y # ys) = (x ∨ y) # (bv_or xs ys)" lemma bv_or_nth: assumes "length l = length r" assumes "i < length l" shows "bv_or l r ! i = (l ! i ∨ r ! i)" using assms proof (induct l r arbitrary: i rule: bv_or.induct) case (2 xx xss yy yss ii) have "ii = 0 ∨ ii > 0" by auto thus ?case proof (elim disjE) assume "ii > 0" then obtain j where J: "ii = Suc j" by (induct ii) simp+ with 2 show ?thesis by simp qed simp qed simp+ lemma bv_or_length: assumes "length l = length r" shows "length (bv_or l r) = length l" using assms by (induct l r rule: bv_or.induct) simp+ lemma bv_or_set_of_bv: assumes "nfa_is_node A p" and "nfa_is_node A q" shows "set_of_bv (bv_or p q) = set_of_bv p ∪ set_of_bv q" using assms by (auto simp: nfa_is_node_def set_of_bv_def bv_or_length bv_or_nth) lemma bv_or_is_node: "⟦nfa_is_node A p; nfa_is_node A q⟧ ⟹ nfa_is_node A (bv_or p q)" by (simp add: bv_or_length nfa_is_node_def) fun subsetbdd where "subsetbdd [] [] bdd = bdd" | "subsetbdd (bdd' # bdds) (b # bs) bdd = (if b then subsetbdd bdds bs (bdd_binop bv_or bdd bdd') else subsetbdd bdds bs bdd)" definition nfa_emptybdd :: "nat ⇒ bool list bdd" where "nfa_emptybdd n = Leaf (replicate n False)" lemma bdd_all_is_node_subsetbdd: assumes "list_all (bdd_all (nfa_is_node A)) (fst A)" and "nfa_is_node A q" shows "bdd_all (nfa_is_node A) (subsetbdd (fst A) q (nfa_emptybdd (length q)))" proof - { fix bdds :: "bool list bdd list" and q :: "bool list" and bd :: "bool list bdd" and n assume "list_all (bdd_all (λl. length l = n)) bdds" and "bdd_all (λl. length l = n) bd" and "length bdds = length q" hence "bdd_all (λl. length l = n) (subsetbdd bdds q bd)" by (induct bdds q bd rule: subsetbdd.induct) (simp add: bdd_all_bdd_binop[of "λl. length l =n" _ "λl. length l = n"] bv_or_length)+ } with assms show ?thesis by (simp add: nfa_is_node_def nfa_emptybdd_def) qed lemma bddh_subsetbdd: assumes "list_all (bddh l) (fst A)" and "bddh l bdd'" and "nfa_is_node A q" shows "bddh l (subsetbdd (fst A) q bdd')" using assms unfolding nfa_is_node_def by (induct ("fst A") q bdd' rule: subsetbdd.induct) (simp add: bddh_binop)+ lemma bdd_lookup_subsetbdd': assumes "length bdds = length q" and "∀x ∈ set bdds. bddh (length ws) x" and "bddh (length ws) obdd" and "⋀bs w. ⟦bs ∈ set bdds; length w = length ws⟧ ⟹ length (bdd_lookup bs w) = c" and "⋀w. length w = length ws ⟹ length (bdd_lookup obdd w) = c" and "a < c" shows "bdd_lookup (subsetbdd bdds q obdd) ws ! a = ((∃i < length q. q ! i ∧ bdd_lookup (bdds ! i) ws ! a) ∨ bdd_lookup obdd ws ! a)" using assms proof (induct bdds q obdd rule: subsetbdd.induct) case (2 bdd' bdds x xs bdd) show ?case proof (cases x) case True with 2 have H: "bdd_lookup (subsetbdd bdds xs (bdd_binop bv_or bdd bdd')) ws ! a = ((∃i<length xs. xs ! i ∧ bdd_lookup (bdds ! i) ws ! a) ∨ bdd_lookup (bdd_binop bv_or bdd bdd') ws ! a)" by (simp add: bddh_binop bdd_lookup_binop bv_or_length) from 2 have "((∃i < length xs. xs ! i ∧ bdd_lookup (bdds ! i) ws ! a) ∨ bdd_lookup (bdd_binop bv_or bdd bdd') ws ! a) = ((∃i < length xs. xs ! i ∧ bdd_lookup (bdds ! i) ws ! a) ∨ (bdd_lookup bdd' ws) ! a ∨ (bdd_lookup bdd ws) ! a)" by (auto simp: bdd_lookup_binop bv_or_nth) also have "… = ((∃i < Suc (length xs). (True # xs) ! i ∧ bdd_lookup ((bdd' # bdds) ! i) ws ! a) ∨ bdd_lookup bdd ws ! a)" (is "((∃i. ?P i) ∨ ?Q ∨ ?R) = ((∃i. ?S i) ∨ ?R)") proof assume "(∃i. ?P i) ∨ ?Q ∨ ?R" thus "(∃i. ?S i) ∨ ?R" by (elim disjE) auto next assume "(∃i. ?S i) ∨ ?R" thus "(∃i. ?P i) ∨ ?Q ∨ ?R" proof (elim disjE) assume "∃i. ?S i" then obtain i where I: "?S i" .. { assume "i = 0" with I have "?Q" by simp } { assume "i ≠ 0" then obtain j where "i = Suc j" by (cases i) simp+ with I have "∃j. ?P j" by auto } with ‹i=0 ⟹ ?Q› show ?thesis by (cases "i=0") simp+ qed simp qed finally have "((∃i<length xs. xs ! i ∧ bdd_lookup (bdds ! i) ws ! a) ∨ bdd_lookup (bdd_binop bv_or bdd bdd') ws ! a) = ((∃i<Suc (length xs). (True # xs) ! i ∧ bdd_lookup ((bdd' # bdds) ! i) ws ! a) ∨ bdd_lookup bdd ws ! a)" by simp with True H show ?thesis by simp next case False with 2 have H: "bdd_lookup (subsetbdd bdds xs bdd) ws ! a = ((∃i < length xs. xs ! i ∧ bdd_lookup (bdds ! i) ws ! a) ∨ bdd_lookup bdd ws ! a)" by simp have "((∃i<length xs. xs ! i ∧ bdd_lookup (bdds ! i) ws ! a) ∨ bdd_lookup bdd ws ! a) = ((∃i<Suc (length xs). (False # xs) ! i ∧ bdd_lookup ((bdd' # bdds) ! i) ws ! a) ∨ bdd_lookup bdd ws ! a)" (is "((∃i. ?S i) ∨ ?R) = ((∃i. ?P i) ∨ ?R)") proof assume "(∃i. ?S i) ∨ ?R" thus "(∃i. ?P i) ∨ ?R" by (elim disjE) auto next assume "(∃i. ?P i) ∨ ?R" thus "(∃i. ?S i) ∨ ?R" proof (elim disjE) assume "∃i. ?P i" then obtain i where "?P i" .. then obtain j where "i = Suc j" by (cases i) simp+ with ‹?P i› show ?thesis by auto qed simp qed with False H show ?thesis by simp qed qed simp+ lemma bdd_lookup_subsetbdd: assumes "wf_nfa N (length ws)" and "nfa_is_node N q" and "a < length (fst N)" shows "bdd_lookup (subsetbdd (fst N) q (nfa_emptybdd (length q))) ws ! a = (∃i< length q. q ! i ∧ bdd_lookup (fst N ! i) ws ! a)" proof - { fix w :: "bool list" assume H: "length w = length ws" from assms have "∀bd ∈ set (fst N). bdd_all (nfa_is_node N) bd" by (simp add: wf_nfa_def list_all_iff) moreover from assms have "∀bd ∈ set (fst N). bddh (length ws) bd" by (simp add: wf_nfa_def list_all_iff) moreover note H ultimately have "∀bd ∈ set (fst N). nfa_is_node N (bdd_lookup bd w)" by (simp add: bdd_all_bdd_lookup) } with assms have "bdd_lookup (subsetbdd (fst N) q (nfa_emptybdd (length q))) ws ! a = ((∃i < length q. q ! i ∧ bdd_lookup (fst N ! i) ws ! a) ∨ bdd_lookup (nfa_emptybdd (length q)) ws ! a)" by (simp add: bdd_lookup_subsetbdd' nfa_is_node_def wf_nfa_def list_all_iff nfa_emptybdd_def) with assms show ?thesis by (auto simp: nfa_emptybdd_def nfa_is_node_def) qed definition nfa_trans :: "nfa ⇒ bool list ⇒ bool list ⇒ bool list" where "nfa_trans A qs bs = bdd_lookup (subsetbdd (fst A) qs (nfa_emptybdd (length qs))) bs" fun nfa_accepting' :: "bool list ⇒ bool list ⇒ bool" where "nfa_accepting' [] bs = False" | "nfa_accepting' as [] = False" | "nfa_accepting' (a # as) (b # bs) = (a ∧ b ∨ nfa_accepting' as bs)" definition nfa_accepting :: "nfa ⇒ bool list ⇒ bool" where "nfa_accepting A = nfa_accepting' (snd A)" lemma nfa_accepting'_set_of_bv: "nfa_accepting' l r = (set_of_bv l ∩ set_of_bv r ≠ {})" proof - have nfa_accepting_help: "⋀as q. nfa_accepting' as q = (∃i. i < length as ∧ i < length q ∧ as ! i ∧ q ! i)" proof - fix as q show "nfa_accepting' as q = (∃i < length as. i < length q ∧ as ! i ∧ q ! i)" proof (induct as q rule: nfa_accepting'.induct) case (3 a as q qs) thus ?case proof (cases "a∧q") case False with 3 have "nfa_accepting' as qs = (∃i < length as. i < length qs ∧ as ! i ∧ qs ! i)" (is "?T = _") by simp also have "… = (∃j < length as. j < length qs ∧ (a#as) ! Suc j ∧ (q#qs) ! Suc j)" by simp also have "… = (∃j < length (a#as). j < length (q#qs) ∧ (a#as) ! j ∧ (q#qs) ! j)" (is "(∃j. ?P j) = (∃j. ?Q j)") proof assume "∃j. ?P j" then obtain j where "?P j" .. hence "?Q (Suc j)" by simp thus "∃j. ?Q j" by (rule exI) next assume "∃j. ?Q j" then obtain j where J: "?Q j" .. with False obtain i where "j = Suc i" by (cases j) simp+ with J have "?P i" by simp thus "∃i. ?P i" by (rule exI) qed also from False have "… = ((a∧q ∧ ?Q 0) ∨ (¬ (a∧q) ∧ (∃j. ?Q j)))" by auto also have "… = ((a ∧ q ∧ (∃j. ?Q j)) ∨ (¬(a∧q) ∧ (∃j. ?Q j)))" by auto also have "… = (∃j. ?Q j)" by auto finally have "?T = (∃j. ?Q j)" . with False show ?thesis by auto qed (auto simp: 3) qed simp+ qed hence "nfa_accepting' l r = (∃i. i < length l ∧ i < length r ∧ l ! i ∧ r ! i)" by simp also have "… = (∃i. i ∈ set_of_bv l ∧ i ∈ set_of_bv r)" by (auto simp: set_of_bv_def) also have "… = (set_of_bv l ∩ set_of_bv r ≠ {})" by auto finally show ?thesis . qed lemma nfa_accepting_set_of_bv: "nfa_accepting A q = (set_of_bv (snd A) ∩ set_of_bv q ≠ {})" by (simp add: nfa_accepting'_set_of_bv nfa_accepting_def) definition nfa_startnode :: "nfa ⇒ bool list" where "nfa_startnode A = (replicate (length (fst A)) False)[0:=True]" locale aut_nfa = fixes A n assumes well_formed: "wf_nfa A n" sublocale aut_nfa < Automaton "nfa_trans A" "nfa_is_node A" "is_alph n" proof fix q a assume Q: "nfa_is_node A q" and A: "is_alph n a" with well_formed have "bdd_all (nfa_is_node A) (subsetbdd (fst A) q (nfa_emptybdd (length q)))" by (simp add: wf_nfa_def bdd_all_is_node_subsetbdd) moreover from well_formed Q have "bddh n (subsetbdd (fst A) q (nfa_emptybdd (length q)))" by (simp add: wf_nfa_def nfa_emptybdd_def bddh_subsetbdd) with A have "bddh (length a) (subsetbdd (fst A) q (nfa_emptybdd (length q)))" by (simp add: is_alph_def) ultimately have "nfa_is_node A (bdd_lookup (subsetbdd (fst A) q (nfa_emptybdd (length q))) a)" by (simp add: bdd_all_bdd_lookup) then show "nfa_is_node A (nfa_trans A q a)" by (simp add: nfa_trans_def) qed context aut_nfa begin lemmas trans_is_node = trans_is_node lemmas steps_is_node = steps_is_node lemmas reach_is_node = reach_is_node end lemmas nfa_trans_is_node = aut_nfa.trans_is_node [OF aut_nfa.intro] lemmas nfa_steps_is_node = aut_nfa.steps_is_node [OF aut_nfa.intro] lemmas nfa_reach_is_node = aut_nfa.reach_is_node [OF aut_nfa.intro] abbreviation "nfa_steps A ≡ foldl (nfa_trans A)" abbreviation "nfa_accepts A ≡ accepts (nfa_trans A) (nfa_accepting A) (nfa_startnode A)" abbreviation "nfa_reach A ≡ reach (nfa_trans A)" lemma nfa_startnode_is_node: "wf_nfa A n ⟹ nfa_is_node A (nfa_startnode A)" by (simp add: nfa_is_node_def wf_nfa_def nfa_startnode_def) section ‹Automata Constructions› subsection ‹Negation› definition negate_dfa :: "dfa ⇒ dfa" where "negate_dfa = (λ(t,a). (t, map Not a))" lemma negate_wf_dfa: "wf_dfa (negate_dfa A) l = wf_dfa A l" by (simp add: negate_dfa_def wf_dfa_def dfa_is_node_def split_beta) lemma negate_negate_dfa: "negate_dfa (negate_dfa A) = A" proof (induct A) case (Pair t a) thus ?case by (induct a) (simp add: negate_dfa_def)+ qed lemma dfa_accepts_negate: assumes "wf_dfa A n" and "list_all (is_alph n) bss" shows "dfa_accepts (negate_dfa A) bss = (¬ dfa_accepts A bss)" proof - have "dfa_steps (negate_dfa A) 0 bss = dfa_steps A 0 bss" by (simp add: negate_dfa_def dfa_trans_def [abs_def] split_beta) moreover from assms have "dfa_is_node A (dfa_steps A 0 bss)" by (simp add: dfa_steps_is_node dfa_startnode_is_node) ultimately show ?thesis using assms by (simp add: accepts_def dfa_accepting_def wf_dfa_def dfa_is_node_def negate_dfa_def split_beta) qed subsection ‹Product Automaton› definition prod_succs :: "dfa ⇒ dfa ⇒ nat × nat ⇒ (nat × nat) list" where "prod_succs A B = (λ(i, j). add_leaves (bdd_binop Pair (fst A ! i) (fst B ! j)) [])" definition "prod_is_node A B = (λ(i, j). dfa_is_node A i ∧ dfa_is_node B j)" definition prod_invariant :: "dfa ⇒ dfa ⇒ nat option list list × (nat × nat) list ⇒ bool" where "prod_invariant A B = (λ(tab, ps). length tab = length (fst A) ∧ (∀tab'∈set tab. length tab' = length (fst B)))" definition "prod_ins = (λ(i, j). λ(tab, ps). (tab[i := (tab ! i)[j := Some (length ps)]], ps @ [(i, j)]))" definition prod_memb :: "nat × nat ⇒ nat option list list × (nat × nat) list ⇒ bool" where "prod_memb = (λ(i, j). λ(tab, ps). tab ! i ! j ≠ None)" definition prod_empt :: "dfa ⇒ dfa ⇒ nat option list list × (nat × nat) list" where "prod_empt A B = (replicate (length (fst A)) (replicate (length (fst B)) None), [])" definition prod_dfs :: "dfa ⇒ dfa ⇒ nat × nat ⇒ nat option list list × (nat × nat) list" where "prod_dfs A B x = gen_dfs (prod_succs A B) prod_ins prod_memb (prod_empt A B) [x]" definition binop_dfa :: "(bool ⇒ bool ⇒ bool) ⇒ dfa ⇒ dfa ⇒ dfa" where "binop_dfa f A B = (let (tab, ps) = prod_dfs A B (0, 0) in (map (λ(i, j). bdd_binop (λk l. the (tab ! k ! l)) (fst A ! i) (fst B ! j)) ps, map (λ(i, j). f (snd A ! i) (snd B ! j)) ps))" locale prod_DFS = fixes A B n assumes well_formed1: "wf_dfa A n" and well_formed2: "wf_dfa B n" sublocale prod_DFS < DFS "prod_succs A B" "prod_is_node A B" "prod_invariant A B" prod_ins prod_memb "prod_empt A B" apply unfold_locales apply (simp add: prod_memb_def prod_ins_def prod_invariant_def prod_is_node_def split_paired_all dfa_is_node_def) apply (case_tac "a = aa") apply (case_tac "b = ba") apply auto[3] apply (simp add: prod_memb_def prod_empt_def prod_is_node_def split_paired_all dfa_is_node_def) apply (insert well_formed1 well_formed2)[] apply (simp add: prod_is_node_def prod_succs_def split_paired_all dfa_is_node_def wf_dfa_def) apply (drule conjunct1 [OF conjunct2])+ apply (simp add: list_all_iff) apply (rule ballI) apply (simp add: split_paired_all) apply (drule subsetD [OF add_leaves_binop_subset [where xs="[]" and ys="[]", simplified]]) apply clarify apply (drule_tac x="fst A ! a" in bspec) apply simp apply (drule_tac x="fst B ! b" in bspec) apply simp apply (simp add: 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)) ! s⇩_{1}! s⇩_{2}= Some m ∧ dfa_is_node A s⇩_{1}∧ dfa_is_node B s⇩_{2}) = (dfa_reach A 0 bss s⇩_{1}∧ dfa_reach B 0 bss s⇩_{2})" proof - let ?tr = "map (λ(i, j). bdd_binop (λk l. the (fst (prod_dfs A B (0,0)) ! k ! l)) (fst A ! i) (fst B ! j)) (snd (prod_dfs A B (0,0)))" have T: "?tr = fst (binop_dfa f A B)" by (simp add: binop_dfa_def split_beta) from well_formed1 well_formed2 have is_node_s1_s2: "prod_is_node A B (0, 0)" by (simp add: prod_is_node_def wf_dfa_def dfa_is_node_def) from well_formed1 well_formed2 have s1: "dfa_is_node A 0" and s2: "dfa_is_node B 0" by (simp add: dfa_is_node_def wf_dfa_def)+ from s1 s2 have start: "fst (prod_dfs A B (0,0)) ! 0 ! 0 = Some 0" by (rule prod_dfs_start) show "(∃m. dfa_reach (binop_dfa f A B) 0 bss m ∧ fst (prod_dfs A B (0, 0)) ! s⇩_{1}! s⇩_{2}= Some m ∧ dfa_is_node A s⇩_{1}∧ dfa_is_node B s⇩_{2}) = (dfa_reach A 0 bss s⇩_{1}∧ dfa_reach B 0 bss s⇩_{2})" (is "(∃m. ?lhs1 m ∧ ?lhs2 m ∧ ?lhs3 ∧ ?lhs4) = ?rhs" is "?lhs = _") proof assume "∃m. ?lhs1 m ∧ ?lhs2 m ∧ ?lhs3 ∧ ?lhs4" then obtain m where lhs: "?lhs1 m" "?lhs2 m" "?lhs3" "?lhs4" by auto from lhs bss show ?rhs proof (induct arbitrary: s⇩_{1}s⇩_{2}) case Nil from is_node_s1_s2 s1 s2 ‹dfa_is_node A s⇩_{1}› ‹dfa_is_node B s⇩_{2}› have "(0, 0) = (s⇩_{1}, s⇩_{2})" using start ‹fst (prod_dfs A B (0,0)) ! s⇩_{1}! s⇩_{2}= Some 0› by (rule prod_dfs_inj) moreover have "dfa_reach A 0 [] 0" by (rule reach_nil) moreover have "dfa_reach B 0 [] 0" by (rule reach_nil) ultimately show ?case by simp next case (snoc j bss bs s⇩_{1}s⇩_{2}) then have "length bs = n" by (simp add: is_alph_def) moreover from binop_wf_dfa have "dfa_is_node (binop_dfa f A B) 0" by (simp add: dfa_is_node_def wf_dfa_def) with snoc binop_wf_dfa [of f] have "dfa_is_node (binop_dfa f A B) j" by (simp add: dfa_reach_is_node) then have j: "j < length (snd (prod_dfs A B (0,0)))" by (simp add: binop_dfa_def dfa_is_node_def split_beta) with prod_dfs_bij [OF is_node_s1_s2, of "fst (snd (prod_dfs A B (0,0)) ! j)" "snd (snd (prod_dfs A B (0,0)) ! j)"] have j_tr1: "dfa_is_node A (fst (snd (prod_dfs A B (0,0)) ! j))" and j_tr2: "dfa_is_node B (snd (snd (prod_dfs A B (0,0)) ! j))" and Some_j: "fst (prod_dfs A B (0,0)) ! fst (snd (prod_dfs A B (0,0)) ! j) ! snd (snd (prod_dfs A B (0,0)) ! j) = Some j" by auto note j_tr1 j_tr2 s1 s2 Some_j ultimately obtain k where k: "fst (prod_dfs A B (0,0)) ! dfa_trans A (fst (snd (prod_dfs A B (0, 0)) ! j)) bs ! dfa_trans B (snd (snd (prod_dfs A B (0, 0)) ! j)) bs = Some k" and s_tr1': "dfa_is_node A (dfa_trans A (fst (snd (prod_dfs A B (0,0)) ! j)) bs)" and s_tr2': "dfa_is_node B (dfa_trans B (snd (snd (prod_dfs A B (0,0)) ! j)) bs)" by (rule prod_dfs_statetrans) from well_formed1 well_formed2 j_tr1 j_tr2 snoc have lh: "bddh (length bs) (fst A ! fst (snd (prod_dfs A B (0,0)) ! j))" and rh: "bddh (length bs) (fst B ! snd (snd (prod_dfs A B (0,0)) ! j))" by (auto simp: wf_dfa_def dfa_is_node_def list_all_iff is_alph_def) from snoc(3)[unfolded dfa_trans_def binop_dfa_def Let_def split_beta fst_conv nth_map[OF j] bdd_lookup_binop[OF lh,OF rh], folded dfa_trans_def] k have "fst (prod_dfs A B (0,0)) ! s⇩_{1}! s⇩_{2}= Some k" by simp with is_node_s1_s2 ‹dfa_is_node A s⇩_{1}› ‹dfa_is_node B s⇩_{2}› s_tr1' s_tr2' have "(s⇩_{1}, s⇩_{2}) = (dfa_trans A (fst (snd (prod_dfs A B (0,0)) ! j)) bs, dfa_trans B (snd (snd (prod_dfs A B (0,0)) ! j)) bs)" using k by (rule prod_dfs_inj) moreover from snoc Some_j j_tr1 j_tr2 have "dfa_reach A 0 bss (fst (snd (prod_dfs A B (0,0)) ! j))" by simp hence "dfa_reach A 0 (bss @ [bs]) (dfa_trans A (fst (snd (prod_dfs A B (0,0)) ! j)) bs)" by (rule reach_snoc) moreover from snoc Some_j j_tr1 j_tr2 have "dfa_reach B 0 bss (snd (snd (prod_dfs A B (0,0)) ! j))" by simp hence "dfa_reach B 0 (bss @ [bs]) (dfa_trans B (snd (snd (prod_dfs A B (0,0)) ! j)) bs)" by (rule reach_snoc) ultimately show "dfa_reach A 0 (bss @ [bs]) s⇩_{1}∧ dfa_reach B 0 (bss @ [bs]) s⇩_{2}" by simp qed next assume ?rhs hence reach: "dfa_reach A 0 bss s⇩_{1}" "dfa_reach B 0 bss s⇩_{2}" by simp_all then show ?lhs using bss proof (induct arbitrary: s⇩_{2}) case Nil with start s1 s2 show ?case by (auto intro: reach_nil simp: reach_nil_iff) next case (snoc j bss bs s⇩_{2}) from snoc(3) obtain s⇩_{2}' where reach_s2': "dfa_reach B 0 bss s⇩_{2}'" and s2': "s⇩_{2}= dfa_trans B s⇩_{2}' bs" by (auto simp: reach_snoc_iff) from snoc(2) [OF reach_s2'] snoc(4) obtain m where reach_m: "dfa_reach (binop_dfa f A B) 0 bss m" and m: "fst (prod_dfs A B (0,0)) ! j ! s⇩_{2}' = Some m" and j: "dfa_is_node A j" and s2'': "dfa_is_node B s⇩_{2}'" by auto from snoc have "list_all (is_alph n) bss" by simp with binop_wf_dfa reach_m dfa_startnode_is_node[OF binop_wf_dfa] have m_less: "dfa_is_node (binop_dfa f A B) m" by (rule dfa_reach_is_node) from is_node_s1_s2 m j s2'' have m': "(m < length (snd (prod_dfs A B (0,0))) ∧ snd (prod_dfs A B (0,0)) ! m = (j, s⇩_{2}'))" by (simp add: prod_dfs_bij [symmetric]) with j s2'' have "dfa_is_node A (fst (snd (prod_dfs A B (0,0)) ! m))" "dfa_is_node B (snd (snd (prod_dfs A B (0,0)) ! m))" by simp_all with well_formed1 well_formed2 snoc have bddh: "bddh (length bs) (fst A ! fst (snd (prod_dfs A B (0,0)) ! m))" "bddh (length bs) (fst B ! snd (snd (prod_dfs A B (0,0)) ! m))" by (simp add: wf_dfa_def is_alph_def dfa_is_node_def list_all_iff)+ from snoc have "length bs = n" by (simp add: is_alph_def) then obtain k where k: "fst (prod_dfs A B (0,0)) ! dfa_trans A j bs ! dfa_trans B s⇩_{2}' bs = Some k" and s_tr1: "dfa_is_node A (dfa_trans A j bs)" and s_tr2: "dfa_is_node B (dfa_trans B s⇩_{2}' bs)" using j s2'' s1 s2 m by (rule prod_dfs_statetrans) show ?case apply (rule exI) apply (simp add: s2') apply (intro conjI) apply (rule reach_snoc) apply (rule reach_m) apply (cut_tac m_less) apply (simp add: dfa_trans_def binop_dfa_def split_beta dfa_is_node_def) apply (simp add: bddh bdd_lookup_binop split_beta) apply (simp add: dfa_trans_def[symmetric] m' k) apply (rule s_tr1) apply (rule s_tr2) done qed qed qed lemma binop_dfa_steps: assumes X: "list_all (is_alph n) bs" shows "snd (binop_dfa f A B) ! dfa_steps (binop_dfa f A B) 0 bs = f (snd A ! dfa_steps A 0 bs) (snd B ! dfa_steps B 0 bs)" (is "?as3 ! dfa_steps ?A 0 bs = ?rhs") proof - note 2 = dfa_startnode_is_node[OF well_formed1] note 5 = dfa_startnode_is_node[OF well_formed2] note B = dfa_startnode_is_node[OF binop_wf_dfa] define tab where "tab = fst (prod_dfs A B (0,0))" define ps where "ps = snd (prod_dfs A B (0,0))" from tab_def ps_def have prod: "prod_dfs A B (0,0) = (tab, ps)" by simp define s1 where "s1 = dfa_steps A 0 bs" define s2 where "s2 = dfa_steps B 0 bs" with s1_def have "dfa_reach A 0 bs s1" and "dfa_reach B 0 bs s2" by (simp add: reach_def)+ with X have "∃m. dfa_reach ?A 0 bs m ∧ fst (prod_dfs A B (0, 0)) ! s1 ! s2 = Some m ∧ dfa_is_node A s1 ∧ dfa_is_node B s2" by (simp add: binop_dfa_reachable) with tab_def have "∃m. dfa_reach ?A 0 bs m ∧ tab ! s1 ! s2 = Some m ∧ dfa_is_node A s1 ∧ dfa_is_node B s2" by simp then obtain m where R: "dfa_reach ?A 0 bs m" and M: "tab ! s1 ! s2 = Some m" and s1: "dfa_is_node A s1" and s2: "dfa_is_node B s2" by blast hence M': "m = dfa_steps ?A 0 bs" by (simp add: reach_def) from B X R binop_wf_dfa [of f] have mL: "dfa_is_node ?A m" by (simp add: dfa_reach_is_node) from 2 5 M s1 s2 have bij: "m < length (snd (prod_dfs A B (0, 0))) ∧ snd (prod_dfs A B (0, 0)) ! m = (s1, s2)" unfolding tab_def by (simp add: prod_dfs_bij[symmetric] prod_is_node_def) with mL have "snd (binop_dfa f A B) ! m = f (snd A ! s1) (snd B ! s2)" by (simp add: binop_dfa_def split_beta dfa_is_node_def) with M' s1_def s2_def show "snd ?A ! dfa_steps ?A 0 bs = f (snd A ! dfa_steps A 0 bs) (snd B ! dfa_steps B 0 bs)" by simp qed end lemma binop_wf_dfa: assumes A: "wf_dfa A n" and B: "wf_dfa B n" shows "wf_dfa (binop_dfa f A B) n" proof - from A B interpret prod_DFS A B n by unfold_locales show ?thesis by (rule binop_wf_dfa) qed theorem binop_dfa_accepts: assumes A: "wf_dfa A n" and B: "wf_dfa B n" and X: "list_all (is_alph n) bss" shows "dfa_accepts (binop_dfa f A B) bss = f (dfa_accepts A bss) (dfa_accepts B bss)" proof - from A B interpret prod_DFS A B n by unfold_locales from X show ?thesis by (simp add: accepts_def dfa_accepting_def binop_dfa_steps) qed definition and_dfa :: "dfa ⇒ dfa ⇒ dfa" where "and_dfa = binop_dfa (∧)" lemma and_wf_dfa: assumes "wf_dfa M n" and "wf_dfa N n" shows "wf_dfa (and_dfa M N) n" using assms by (simp add: and_dfa_def binop_wf_dfa) lemma and_dfa_accepts: assumes "wf_dfa M n" and "wf_dfa N n" and "list_all (is_alph n) bs" shows "dfa_accepts (and_dfa M N) bs = (dfa_accepts M bs ∧ dfa_accepts N bs)" using assms by (simp add: binop_dfa_accepts and_dfa_def) definition or_dfa :: "dfa ⇒ dfa ⇒ dfa" where "or_dfa = binop_dfa (∨)" lemma or_wf_dfa: assumes "wf_dfa M n" and "wf_dfa N n" shows "wf_dfa (or_dfa M N) n" using assms by (simp add: or_dfa_def binop_wf_dfa) lemma or_dfa_accepts: assumes "wf_dfa M n" and "wf_dfa N n" and "list_all (is_alph n) bs" shows "dfa_accepts (or_dfa M N) bs = (dfa_accepts M bs ∨ dfa_accepts N bs)" using assms by (simp add: binop_dfa_accepts or_dfa_def) definition imp_dfa :: "dfa ⇒ dfa ⇒ dfa" where "imp_dfa = binop_dfa (⟶)" lemma imp_wf_dfa: assumes "wf_dfa M n" and "wf_dfa N n" shows "wf_dfa (imp_dfa M N) n" using assms by (simp add: binop_wf_dfa imp_dfa_def) lemma imp_dfa_accepts: assumes "wf_dfa M n" and "wf_dfa N n" and "list_all (is_alph n) bs" shows "dfa_accepts (imp_dfa M N) bs = (dfa_accepts M bs ⟶ dfa_accepts N bs)" using assms by (auto simp add: binop_dfa_accepts imp_dfa_def) subsection ‹Transforming DFAs to NFAs› definition nfa_of_dfa :: "dfa ⇒ nfa" where "nfa_of_dfa = (λ(bdd,as). (map (bdd_map (λq. (replicate (length bdd) False)[q:=True])) bdd, as))" lemma dfa2wf_nfa: assumes "wf_dfa M n" shows "wf_nfa (nfa_of_dfa M) n" proof - have "⋀a. dfa_is_node M a ⟹ nfa_is_node (nfa_of_dfa M) ((replicate (length (fst M)) False)[a:=True])" by (simp add: dfa_is_node_def nfa_is_node_def nfa_of_dfa_def split_beta) hence "⋀bdd. bdd_all (dfa_is_node M) bdd ⟹ bdd_all (nfa_is_node (nfa_of_dfa M)) (bdd_map (λq. (replicate (length (fst M)) False)[q:=True]) bdd)" by (simp add: bdd_all_bdd_map) with assms have "list_all (bdd_all (nfa_is_node (nfa_of_dfa M))) (fst (nfa_of_dfa M))" by (simp add: list_all_iff split_beta nfa_of_dfa_def wf_dfa_def) with assms show ?thesis by (simp add: wf_nfa_def wf_dfa_def nfa_of_dfa_def split_beta list_all_iff bddh_bdd_map) qed lemma replicate_upd_inj: "⟦q < n; (replicate n False)[q:=True] = (replicate n False)[p:=True]⟧ ⟹ (q = p)" (is "⟦_ ;?lhs = ?rhs⟧ ⟹ _") proof - assume q: "q < n" and r: "?lhs = ?rhs" { assume "p ≠ q" with q have "?lhs ! q = True" by simp moreover from ‹p ≠ q› q have "?rhs ! q = False" by simp ultimately have "?lhs ≠ ?rhs" by auto } with r show "q = p" by auto qed lemma nfa_of_dfa_reach': assumes V: "wf_dfa M l" and X: "list_all (is_alph l) bss" and N: "n1 = (replicate (length (fst M)) False)[q:=True]" and Q: "dfa_is_node M q" and R: "nfa_reach (nfa_of_dfa M) n1 bss n2" shows "∃p. dfa_reach M q bss p ∧ n2 = (replicate (length (fst M)) False)[p:=True]" proof - from R V X N Q show ?thesis proof induct case Nil hence "dfa_reach M q [] q" by (simp add: reach_nil) with Nil show ?case by auto next case (snoc j bss bs) hence N1: "nfa_is_node (nfa_of_dfa M) n1" by (simp add: nfa_is_node_def nfa_of_dfa_def split_beta) from snoc have V2: "wf_nfa (nfa_of_dfa M) l" by (