[isabelle] Using schematic_lemma to avoid boilerplate


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.

Then I found that I can use schematic_lemma:

schematic_lemma caseB:
   assumes "D x"
   shows "PROP ?C"
using D_X[OF `D x`] D_Y[OF `D Y`]
by (fact caseA)

I can figure this might be seen as abuse of the schematic_ construct. So
my question is: Is this intended to work? Or is this only working by
accident? Is there a better way of doing it (without having to spell out
all the cases)?


René Neumann

Institut für Informatik (I7)
Technische Universität München
Boltzmannstr. 3
85748 Garching b. München

Tel: +49-89-289-17232
Office: MI 03.11.055

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