[isabelle] Range of a record-valued function

[Holger Blasum]

Dear all,

this is probably an easy one, I am trying to define the range
of a function that uses pattern matching on a datatype (num_t).
I can show it by "auto" in lemma f_range (see below) on
a function that is num_t-valued. I seem to be missing an intermediate
step once I am wrapping that num_t into a record num_wrapper_t,
(see proof attempt at f_wrapper_def below).

theory record_valued_function
imports Main
begin

datatype num_t = ONE | TWO

(* The following lemma has been proved by "auto". *)

definition f::"num_t => nat set" where
"f n = (if (n = ONE) then {1} else {2})"
lemma f_range: "Union ({x. EX n. x = f n}) = {1,2}"
proof-
from f_def show ?thesis by auto
qed

(* This is the lemma where I am missing an intermediate step. *)

record num_wrapper_t = num::num_t
definition f_wrapper::"num_wrapper_t => nat set" where
"f_wrapper r = (if ((num r) = ONE) then {1} else {2})"
lemma f_wrapper_range: "Union ({x. (EX r. x = f_wrapper r)}) = {1,2}"
proof-
from f_wrapper_def have r1: "ALL r. num r = ONE
--> f_wrapper r = {1}" by fastforce
from f_wrapper_def have r2: "ALL r. num r = TWO
--> f_wrapper r = {2}" by fastforce
from r1 and r2 and f_wrapper_def show ?thesis
sorry <-- fails

Suggestions on how to complete the second lemma would be welcome,

--
Holger Blasum, SYSGO

[Thomas Sewell]

You can solve this problem via:

lemma f_wrapper_range: "Union ({x. (EX r. x = f_wrapper r)}) = {1,2}"

by (auto simp add: f_wrapper_def num_wrapper_t.splits)

To be slightly clearer:

lemma f_wrapper_range: "Union ({x. (EX r. x = f_wrapper r)}) = {1,2}"
proof -

have exs: "EX x. num x = ONE" "EX x. num x ~= ONE"
by (simp_all add: num_wrapper_t.splits exI[where x=TWO])
thus ?thesis
by (auto simp add: f_wrapper_def)
qed

What you need to show is that there are objects in the num_wrapper_t
type with num taking both values. That's not syntactically clear: if num
x had a more limited range, f_wrapper would too.

Yours,
Thomas.

[Tjark Weber]

On Wed, 2012-09-26 at 11:08 +0200, Holger Blasum wrote:
> lemma f_range: "Union ({x. EX n. x = f n}) = {1,2}"
> proof-
> from f_def show ?thesis by auto
> qed

Main already provides image (`) and range operators, cf. Section 4 of
http://www.cl.cam.ac.uk/research/hvg/isabelle/dist/Isabelle2012/doc/main.pdf

So you could simply claim "range f = {1,2}".

Best regards,
Tjark

[Holger Blasum]

Hi Thomas, Tjark,

On 09-27, Thomas Sewell wrote:
> You can solve this problem via:

> ... simp_all add: num_wrapper_t.splits ...

I realize I never followed up this on. Yup, worked.
The "splits" lemma also made me curious about what exactly gets
introduced after declaring a datatype and a record,
so I also played a bit with "print_theorems" after declaring
the datatype and the record - useful information.

Thanks,

--
Holger