Stream: General

Topic: ✔ enumerating non-constructor patterns

Chengsong Tan (Feb 09 2022 at 19:31):

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

Mathias Fleury (Feb 09 2022 at 19:32):

Suc 0, not 1

Chengsong Tan (Feb 09 2022 at 19:34):

My bad....... I thought it was Isabelle chars causing the problem.....
Thank you Mathias!

Notification Bot (Feb 09 2022 at 19:34):

Chengsong Tan has marked this topic as resolved.

Notification Bot (Feb 09 2022 at 19:34):

Chengsong Tan has marked this topic as unresolved.

Notification Bot (Feb 09 2022 at 19:34):

Chengsong Tan has marked this topic as resolved.

Last updated: Apr 25 2024 at 04:18 UTC