[isabelle] Novice question about functions



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
 
--
Victor Porton - http://portonvictor.org


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