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"
     sorry

   lemma l2: "(\<And> E E'. E' \<subseteq> E ==> P E ==> P E')"
     sorry

writing
   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.


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.