[isabelle] Option type question

[Manfred Kerber]

Dear All,

I am not too familiar with option types and have a question of how to
best use them.

More concretely, we have defined a partial function using the option
type and the function is defined on a finite number of real numbers
inside the unit interval. Then we have proved a number of properties
of this function. Now we want to also use an extended version of the
function which is defined in two further points (in 0 and 1) and want
to reuse the original proofs as much as possible.

What is the best way to extend a partial function defined via an
option type so that as much of the structure of the definitions,
theorems, and proofs can be reused?

Many thanks
Manfred

[Thiemann, René]

Dear Manfred,

I see at least two possibilities. Assume your current definition of the
function is:

f :: real => real
f = some_definition

1) You write your extended function like

g = f (0 ↦ 5, 1 ↦ 7)

and then try to prove properties of g by reusing the existing theorems for f.

2) You change the definition of f itself to

f = some_definition (0 ↦ 5, 1 ↦ 7)

and then add a case-anaylsis on x = 0, x = 1, x != 0,1 to your existing proofs.

I hope some of these approaches is applicable in your case.

Best regards,
René

Post by Manfred Kerber
Dear All,
I am not too familiar with option types and have a question of how to
best use them.
More concretely, we have defined a partial function using the option
type and the function is defined on a finite number of real numbers
inside the unit interval. Then we have proved a number of properties
of this function. Now we want to also use an extended version of the
function which is defined in two further points (in 0 and 1) and want
to reuse the original proofs as much as possible.
What is the best way to extend a partial function defined via an
option type so that as much of the structure of the definitions,
theorems, and proofs can be reused?
Many than