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