Email Gateway (Aug 18 2022 at 16:42): Email Gateway (Aug 18 2022 at 16:42):From: Victor Porton <porton@narod.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
\--
Victor Porton - http://portonvictor.org
Email Gateway (Aug 18 2022 at 16:42):From: Lawrence Paulson <lp15@cam.ac.uk>
I have two suggestions. First, please base any set theory development on either Main_ZF or Main_ZFC, which contain full developments of axiomatic set theory, including in the latter case the axiom of choice. The theory ZF, which you currently use, contains only the raw axioms and should be regarded as an internal component of the implementation.
My other suggestion is that you avoid using locales until you have mastered the fundamentals of Isabelle.
Theorems appropriate to your development can be found in the theory func.thy. Use the magnifying glass tool to look for others.
Larry Paulson
Email Gateway (Aug 18 2022 at 16:42):From: Lars Noschinski <noschinl@in.tum.de>
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@in.tum.de>:
On 15.12.2010 23:55, Victor Porton wrote:
theory test
imports ZF
beginI 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
begindefinition "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
Last updated: Nov 21 2024 at 12:39 UTC