Chengsong Tan (Feb 09 2022 at 20:08): Chengsong Tan (Feb 09 2022 at 20:08):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?
Mathias Fleury (Feb 09 2022 at 20:38):even on paper I am not sure what this means… (is i<j? how should the r_1 be ordered?)
Mathias Fleury (Feb 09 2022 at 20:39):all that to say: yes you need your own functions to define that
Mathias Fleury (Feb 09 2022 at 20:40):if you can use a set instead, things are different
Chengsong Tan (Feb 10 2022 at 22:33):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.
Maximilian Schaeffeler (Feb 11 2022 at 08:37):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.
Last updated: Jul 15 2022 at 23:21 UTC