src/HOL/Lex/RegSet_of_nat_DA.thy

added read;

(*  Title:      HOL/Lex/RegSet_of_nat_DA.thy
    ID:         $Id$
    Author:     Tobias Nipkow
    Copyright   1998 TUM

Conversion of deterministic automata into regular sets.

To generate a regual expression, the alphabet must be finite.
regexp needs to be supplied with an 'a list for a unique order

add_Atom d i j r a = (if d a i = j then Union r (Atom a) else r)
atoms d i j as = foldl (add_Atom d i j) Empty as

regexp as d i j 0 = (if i=j then Union (Star Empty) (atoms d i j as)
                        else atoms d i j as
*)

RegSet_of_nat_DA = RegSet + DA +

types 'a nat_next = "'a => nat => nat"

syntax deltas :: 'a nat_next => 'a list => nat => nat
translations "deltas" == "foldl2"

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

(* conversion a la Warshall *)

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

constdefs
 regset_of_DA :: ('a,nat)da => nat => 'a list set
"regset_of_DA A k == UN j:{j. j<k & fin A j}. regset (next A) (start A) j k"

 bounded :: "'a => nat => bool"
"bounded d k == !n. n < k --> (!x. d x n < k)"

end