*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Novice question about functions*From*: Victor Porton <porton at narod.ru>*Date*: Thu, 16 Dec 2010 01:55:14 +0300*Envelope-from*: porton@yandex.ru

I am writing my first real Isabelle theory (indeed very useful for other Isabelle users). I step on the following question.

Let move_fun is an arbitrary function and myset is an arbitrary set (in ZF). How to prove the theorem (marked sorry)?

theory test

imports ZF

begin

locale subtest =

fixes move_fun::"i=>i"

fixes myset::i

begin

definition "move == (lam x:myset. move_fun(x))"

theorem "x: my_set ==> move`x = move_fun(x)" sorry

end

end

imports ZF

begin

locale subtest =

fixes move_fun::"i=>i"

fixes myset::i

begin

definition "move == (lam x:myset. move_fun(x))"

theorem "x: my_set ==> move`x = move_fun(x)" sorry

end

end

--

Victor Porton - http://portonvictor.org

Victor Porton - http://portonvictor.org

**Follow-Ups**:**Re: [isabelle] Novice question about functions***From:*Lawrence Paulson

- Previous by Date: Re: [isabelle] Fw : Re: Question on hypothesis
- Next by Date: Re: [isabelle] Fw : Re: Question on hypothesis
- Previous by Thread: Re: [isabelle] Fw : Re: Question on hypothesis
- Next by Thread: Re: [isabelle] Novice question about functions
- Cl-isabelle-users December 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list