Email Gateway (Aug 18 2022 at 18:51): Email Gateway (Aug 18 2022 at 18:51):From: René Neumann <rene.neumann@in.tum.de>
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.
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)?
Thanks,
René
Email Gateway (Aug 18 2022 at 18:51):From: Brian Huffman <huffman@in.tum.de>
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,
Email Gateway (Aug 18 2022 at 18:51):From: René Neumann <rene.neumann@in.tum.de>
Am 22.12.2011 11:16, schrieb Brian Huffman:
On Wed, Dec 21, 2011 at 9:54 AM, René Neumann <rene.neumann@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é
Last updated: Apr 25 2024 at 20:15 UTC