Corey Richardson

2016-10-06 09:05:38 UTC

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.

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/

cmr

http://octayn.net/