Email Gateway (Aug 19 2022 at 14:56): Email Gateway (Aug 19 2022 at 14:56):From: Joachim Breitner <mail@joachim-breitner.de>
Hi,
I often see this pattern:
I am in some isar context:
case (CaseName a b c d)
and one of the first few facts is finding out something about d:
from CaseName(..)
obtain e f where "d = (e,f)" <proof>
and from now on, I would like to forget d, but I still have to unfold it
in local facts and goals:
from CaseName(3)[unfolded d = _]
have "..." <proof>
...
finally
show ?case unfolding d <proof>
Is there some better way of handling this, where after I have shown "d =
(e,f)" I don’t have to worry about d any more?
I can imagine a command
subst_in_context d = (e,f)
which unfolds d in all local facts and all goals, while retaining their
names (CaseName(2)) etc. until the next "next" or "qed".
Would that be desirable?
Would it be technical possible?
Thanks,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 14:56):From: Tobias Nipkow <nipkow@in.tum.de>
On 18/07/2014 13:02, Joachim Breitner wrote:
Hi,
I often see this pattern:
I am in some isar context:
case (CaseName a b c d)
and one of the first few facts is finding out something about d:
from CaseName(..) obtain e f where "d = (e,f)" <proof>
Here is a naive approximantion of what you want:
where [simp]: "d = (e,f)" <proof>
Tobias
and from now on, I would like to forget d, but I still have to unfold it in
local facts and goals:from CaseName(3)[unfolded
d = _] have "..." <proof> ... finally show
?case unfolding d <proof>Is there some better way of handling this, where after I have shown "d =
(e,f)" I don’t have to worry about d any more?I can imagine a command
subst_in_context
d = (e,f)which unfolds d in all local facts and all goals, while retaining their
names (CaseName(2)) etc. until the next "next" or "qed". Would that be
desirable? Would it be technical possible?Thanks, Joachim
Email Gateway (Aug 19 2022 at 14:56):From: Joachim Breitner <breitner@kit.edu>
Hi,
Of course :-)
But it doesn’t work well in a style with lots of "from fact have "foo"
by (rule lemma)" and "CaseName.IH[OF this]", which I prefer for being
more explicit.
Greetings,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 14:57):From: Lars Noschinski <noschinl@in.tum.de>
What about
note CaseName = CaseName[unfolded d = _]
(although I'd probably use a different name)
Email Gateway (Aug 19 2022 at 14:57):From: Joachim Breitner <breitner@kit.edu>
Hi,
thanks. That’s another nice trick, and an approximation to what I want.
It still doesn’t help me with updating the goal goal (which is probably
harder, as the “goal” as such doesn’t exist. I expect something that
implicitly opens a new context, exports a new ?case and/or thesis, and
then modifies whatever comes out of it at the end).
It also does not change other unnamed local facts containing d.
Greetings,
Joachim
signature.asc
Last updated: Nov 21 2024 at 12:39 UTC