Hi all,

I am trying to prove finiteness of the number of different regular expressions up to a certain size.

My solution is to define a function that enumerates exhaustively all possible regexes up to a given parameter n.

For the atomic character regex, it takes Isabelle's char as argument. Like this:

```
datatype rrexp =
RZERO
| RONE
| RCHAR char
| RSEQ rrexp rrexp
| RALTS "rrexp list"
| RSTAR rrexp
```

That gives me trouble when I am trying to define the rexp_enum function:

Screenshot-2022-02-09-at-19.11.56.png

I was hoping once I defined this function I could give arguments like this:

Screenshot-2022-02-09-at-19.21.16.png

Which gives me a bound on the set size of small regexes:

Screenshot-2022-02-09-at-19.29.57.png

I am wondering how to get around this problem. Maybe simply proving that card set [RCHAR x] < 257?

Thanks a lot,

Chengsong

Suc 0, not 1

My bad....... I thought it was Isabelle chars causing the problem.....

Thank you Mathias!

Chengsong Tan has marked this topic as resolved.

Chengsong Tan has marked this topic as unresolved.

Chengsong Tan has marked this topic as resolved.

Last updated: Feb 27 2024 at 08:17 UTC