Re: [isabelle] Lemma [OF ..] unification with \<And> parts
On Sat, 11 May 2013, C. Diekmann wrote:
given these two lemmata
lemma l1: "(\<And> E E'. E' \<subseteq> E ==> P E ==> P E') ==> D"
lemma l2: "(\<And> E E'. E' \<subseteq> E ==> P E ==> P E')"
thm l1[OF l2]
I expected to get D. However, I get something very strange.
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and