[isabelle] Range of a record-valued function



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





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