src/HOL/Lex/Regset_of_auto.thy

Added an alternativ version of AutoChopper and a theory for the conversion of
automata into regular sets.

(*
Conversion of automata into regular sets.
use_thy"Auto";
*)

Regset_of_auto = List +

(* autos *)

types 'a auto = "'a => nat => nat"

consts deltas :: 'a auto => 'a list => nat => nat
primrec deltas list
"deltas A [] i = i"
"deltas A (x#xs) i = deltas A xs (A x i)"

consts trace :: 'a auto => nat => 'a list => nat list
primrec trace list
"trace A i [] = []"
"trace A i (x#xs) = A x i # trace A (A x i) xs"

(* regular sets *)

constdefs conc :: 'a list set => 'a list set => 'a list set
         "conc A B == {xs@ys | xs ys. xs:A & ys:B}"

consts star :: 'a list set => 'a list set
inductive "star A"
intrs
  NilI   "[] : star A"
  ConsI  "[| a:A; as : star A |] ==> a@as : star A"

(* conversion a la Warshall *)

consts regset_of :: 'a auto => nat => nat => nat => 'a list set
primrec regset_of nat
"regset_of A i j 0 = (if i=j then insert [] {[a] | a. A a i = j}
                             else {[a] | a. A a i = j})"
"regset_of A i j (Suc k) = regset_of A i j k Un
                           conc (regset_of A i k k)
                          (conc (star(regset_of A k k k))
                                (regset_of A k j k))"

end