Re: [isabelle] Using schematic_lemma to avoid boilerplate



Am 22.12.2011 11:16, schrieb Brian Huffman:
> 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]

Unfortunately, this does not work:

When displaying the types we see
thm caseA[OF D_X D_Y]
> [|D (?x2::?'b2); D (?x1::?'b1); C1; Cn|] ==> ?P::bool

i.e. the two x's have different types. The complete form with the "COMP
undouble" then throws an error:

exception TYPE raised (line 109 of "envir.ML"): Variable "?P" has two
distinct types

But as I now learned about COMP (thanks), I created another solution:

lemma lift_to_Dx:
  assumes "X ==> Y ==> PROP S"
  shows "D x ==> PROP S"
using assms
by (simp add: D_X D_Y)

lemmas caseB = caseA[COMP lift_to_Dx]

This looks better than the solution using schematic_lemma, as it is more
self-documenting.

Regards,
René
-- 
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.