Re: [isabelle] Using schematic_lemma to avoid boilerplate
On Wed, Dec 21, 2011 at 9:54 AM, René Neumann <rene.neumann at in.tum.de> wrote:
> I have a case-splitting lemma
> lemma caseA: "[| X; Y; C1; ...; Cn |] ==> P"
> where X and Y are premises and C1 to Cn are the different cases. The
> latter tend to be quite long.
> Now, using the lemmas
> lemma D_X: "D x ==> X"
> lemma D_Y: "D x ==> Y"
> I want to lift caseA to use D x:
> lemma caseB: "[| D x; C1; ...; Cn |] ==> P".
> But I don't want to copy'n'paste the cases, as this a) adds no
> information and b) makes it cumbersome to change the original caseA.
> Therefore I tried
> lemmas caseB = caseA[OF D_X D_Y]
> But this leaves me "[| D x1; D x2; ... " which is not intended.
How about proving a lemma that says you can remove a doubled premise,
and then compose it with your rule:
assumes "PROP P ==> PROP P ==> PROP Q"
shows "PROP P ==> PROP Q"
by (rule assms)
lemmas caseB = caseA[OF D_X D_Y, COMP undouble]
Hope this helps,
This archive was generated by a fusion of
Pipermail (Mailman edition) and