equal
deleted
inserted
replaced
8 |
8 |
9 NA = List + AutoProj + |
9 NA = List + AutoProj + |
10 |
10 |
11 types ('a,'s)na = "'s * ('a => 's => 's set) * ('s => bool)" |
11 types ('a,'s)na = "'s * ('a => 's => 's set) * ('s => bool)" |
12 |
12 |
13 syntax lift :: ('a => 'b set) => 'a set => 'b set |
|
14 translations "lift f A" == "Union(f `` A)" |
|
15 |
|
16 consts delta :: "('a,'s)na => 'a list => 's => 's set" |
13 consts delta :: "('a,'s)na => 'a list => 's => 's set" |
17 primrec delta list |
14 primrec delta list |
18 "delta A [] p = {p}" |
15 "delta A [] p = {p}" |
19 "delta A (a#w) p = lift (delta A w) (next A a p)" |
16 "delta A (a#w) p = Union(delta A w `` next A a p)" |
20 |
17 |
21 constdefs |
18 constdefs |
22 accepts :: ('a,'s)na => 'a list => bool |
19 accepts :: ('a,'s)na => 'a list => bool |
23 "accepts A w == ? q : delta A w (start A). fin A q" |
20 "accepts A w == ? q : delta A w (start A). fin A q" |
24 |
21 |