# Re: [isabelle] Novice question about functions

On 16.12.2010 16:49, Victor Porton wrote:

`[quoting almost everything, because I failed to send the first mail to
``the list]
`> 16.12.2010, 11:18, "Lars Noschinski"<noschinl at in.tum.de>:
>> On 15.12.2010 23:55, Victor Porton wrote:
>>
>>> theory test
>>> imports ZF
>>> begin
>>
>> I don't know about the ZF logic in Isabelle, but you should probably
>> import Main instead. The ZF theory contains only really basic
>> definitions and lemmas, while the Main contains (besides others) a
>> lot of derived lemmas you will need for everyday reasoning.
>>
>>> 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
>>
>> This should probably be "myset" instead of "my_set"?
>>
>> With these two changes, you can prove it just
>

Thanks, it works (after adding Main).
I have one more stupid question:
What (auto simp add: move_def) mean?
Does it mean to first apply auto and then simp? Vice versa? Anything other?

`The auto proof method uses various methods, in particular the
``simplifier. The call above instructs auto to pass this additional lemma
``to its (internal use of) the simplifier.
`
-- Lars

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