*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Using schematic_lemma to avoid boilerplate*From*: René Neumann <rene.neumann at in.tum.de>*Date*: Thu, 22 Dec 2011 13:22:23 +0100*In-reply-to*: <CAAMXsiZ9PF1EU4CAEFS1qCRGtYCTuApHQXyycvXxufN3O5RDXA@mail.gmail.com>*References*: <4EF19EB3.5010809@in.tum.de> <CAAMXsiZ9PF1EU4CAEFS1qCRGtYCTuApHQXyycvXxufN3O5RDXA@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:8.0) Gecko/20111214 Thunderbird/8.0

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

**References**:**[isabelle] Using schematic_lemma to avoid boilerplate***From:*René Neumann

**Re: [isabelle] Using schematic_lemma to avoid boilerplate***From:*Brian Huffman

- Previous by Date: Re: [isabelle] Using schematic_lemma to avoid boilerplate
- Next by Date: [isabelle] Reasoning about types
- Previous by Thread: Re: [isabelle] Using schematic_lemma to avoid boilerplate
- Next by Thread: [isabelle] Reasoning about types
- Cl-isabelle-users December 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list