Re: [isabelle] Range of a record-valued function



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.

On 26/09/12 19:08, Holger Blasum wrote:
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






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