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.