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
> 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
>> 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
>>> 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and