[isabelle] Help defining a mutually recursive function



Greetings,

In a theory I'm working on, I'm having challenges defining a mutually
recursive function.

Here's the repository and the particular function:

https://gitlab.com/cmr/rust-semantics/blob/unsigned/MIR_SimpleEvals.thy#L38

I think I need to prove that read_array does not make a larger "t" for
the higher-order function passed in. I'm not sure how to do this either.

pat_completeness auto also doesn't show completeness of the pattern
matches, which I do not understand. They seem complete to me at least!

I also suspect I'll need some congruence rule for read_array, but even
after studying examples of congruence rules from the functions.pdf and
the Isabelle libraries, I'm not sure what it should be.

Thanks for any help.

-- 
cmr
http://octayn.net/

Attachment: signature.asc
Description: OpenPGP digital signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.