I was trying to define a list using comprehension but got complaints from Isabelle:

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

What I was trying to achieve is to build larger regular expressions with smaller ones recursively:

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

What am I missing here?

Or is it the case that there is no clean way for doing this, that I have to do zip [0..n] [n..0] and define a convolution-like

recursive function for generation?

even on paper I am not sure what this means… (is i<j? how should the r_1 be ordered?)

all that to say: yes you need your own functions to define that

if you can use a set instead, things are different

Mathias Fleury said:

if you can use a set instead, things are different

Thank you!

I tried using set, but get the following:

Screenshot-2022-02-10-at-22.29.49.png

Any idea why the case and how do I fix this?

https://stackoverflow.com/questions/67092973/how-to-define-a-function-map-from-one-set-to-another-f-a-b-in-isabelle

This I found sadly does not help.

Hi,

to define a (recursive) function, you have to prove 2 things: completeness+compatibility of patterns and termination. Both are proved automatically by the command "fun".

In your case, the automatic proof does not work, in this case you use the command "function":

```
context notes rev_conj_cong[fundef_cong] begin
function (sequential) rexp_enum :: "nat ⇒ rrexpr set" where
"rexp_enum 0 = {}" |
"rexp_enum (Suc 0) = {}" |
"rexp_enum (Suc n) = {(RSEQ r1 r2) | r1 r2 i j. r1 ∈ rexp_enum i ∧ r2 ∈ rexp_enum j ∧ i + j = n}"
by pat_completeness auto
termination
by (relation "measure size") auto
end
```

For pattern completeness+comatibility we add `(sequential)`

after `function`

and prove it using `by pat_completeness auto`

(this is quite standard).

For the considerations regarding termination, I refer to

https://stackoverflow.com/questions/33379349/termination-proof-with-functions-using-set-comprehensions

This tackles a very similar definition.

The "functions" tutorial (in Jedit on the upper left: Documentation -> Isabelle Tutorials -> functions) gives you more information about termination proofs.

Maximilian Schaeffeler said:

This helps!

The rev_conj_cong is still a bit mysterious to me, but I can make now the termination proof work.

Thank you!

Chengsong Tan has marked this topic as resolved.

Last updated: Jun 06 2023 at 23:15 UTC