Email Gateway (Aug 19 2022 at 11:04): Email Gateway (Aug 19 2022 at 11:04):From: Tobias Nipkow <nipkow@in.tum.de>
Am 11/05/2013 18:12, schrieb C. Diekmann:
Hello,
given these two lemmata
lemma l1: "(\<And> E E'. E' \<subseteq> E ==> P E ==> P E') ==> D"
sorrylemma l2: "(\<And> E E'. E' \<subseteq> E ==> P E ==> P E')"
sorrywriting
thm l1[OF l2]
I expected to get D. However, I get something very strange. I get
(\<And>E E'. E' \<subseteq> E ==> ?P E ==> ?E'1 E E' \<subseteq> ?E1 E E')
==> (\<And>E E'. E' ⊆ E ==> ?P E ==> ?P1 E E' (?E1 E E')) ==> ?D
[%E E'. ?P1 E E' (?E'1 E E') =?= %E. ?P]
OF treats !! and ==> specially and lifts l2 over l1. The same thing happens when
you apply a rule to a proof state with !! and ==>. In the latter situation you
can prevent that by using `fact' instead of rule, but I don't know if there is
an analogue for OF. Would like to have that from time to time, too.
Tobias
What am I doing wrong, what is happening? In lemma l1, I conclude D
from some (anti-monotonicity) of P. In lemma l2 I show this
anti-monotonicity. Is there a better way to express this?Symbols: \<And> corresponds to /\, or !! written in ASCII.
Regards
Cornelius
Email Gateway (Aug 19 2022 at 11:04):From: Lawrence Paulson <lp15@cam.ac.uk>
"What's happening" is a technical question about Isabelle's internals, but the other question is whether you really need to do things this way. The purpose of meta-level connectives such as !! is to create a framework in which proofs can be constructed. If you are doing things with the framework itself, then to some extent you become an implementer and you have to expect things to become very tricky. But there may be a way to conduct your proof within the style shown in the various tutorials.
Larry
Email Gateway (Aug 19 2022 at 11:05):From: Makarius <makarius@sketis.net>
As already pointed out by Larry, rule composition via "OF" (or "THEN" with
different argument order), or "rule" as a proof method works exactly like
that. You should study relevant Isabelle documentation until you expect
the correct outcome and don't consider it to be strange. This is about
higher-order natural deduction in Isabelle/Pure. Applications should not
step out of that comfortable environment without good reason (which means
you need to understand first what is its very purpose).
Since contemporary Isabelle has a bit too many manuals to keep an
overview, it might help to look at the "Old Introduction to Isabelle"
manual -- where "Isabelle" means Isabelle/Pure, not Isabelle/HOL -- or the
paper "The next 700 theorem provers" by Larry Paulson, 1990.
Makarius
Email Gateway (Aug 19 2022 at 11:05):From: "C. Diekmann" <diekmann@in.tum.de>
Thank you all for your answers. Today I learned that I want to use !
(∀), the ordinary FOL all quantifier.
Email Gateway (Aug 19 2022 at 11:05):From: Lawrence Paulson <lp15@cam.ac.uk>
Another possibility might be to structure your proof something like this:
have "(\<And> E E'. E' \<subseteq> E ==> P E ==> P E')" sorry
hence "D"
Larry
Last updated: Apr 27 2024 at 01:05 UTC