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:
> Hi,
>
> 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:

lemma undouble:
  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,

- Brian





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