Re: [isabelle] includes bundle works only in first case
thanks for the explanation.
I have never tried this. So far, I only used "using <facts>" and "unfolding
<some_def>". The latter always worked on all goals and the former affected all
goals if used with the right initial method (-, simp_all, auto, etc.), so I
would have expected that something similar applies to including.
So yes, it is all within the normal parameters of Isar, despite the potential
surprise. The above example indicates that the new 'including' command is better
not used before a proof block. BTW, the longer existing 'using', with its later
addition to affect the context, already produces the same effect:
lemma "x = x" "y = y"
show "y = y" ..
In my real use case, each goal had the full fix-assume-show chain, so the next
was necessary there.
In the example above you are using 'next' as if would "separate subgoals", but
this is not really its meaning. Plain 'show' statements do not have to be
I read about that alternative, but I actually prefer "including" over
"includes", because including does not clutter the statement of the lemma with
hints to the prover.
Here is an alternative form that includes a bundle in the context of a toplevel
shows "test xs = " and "test ys = "
show "test xs = " by simp
next -- "redundant"
show "test ys = " by simp
Karlsruher Institut für Technologie
Am Fasanengarten 5, Geb. 50.34, Raum 025
Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum
in der Helmholtz-Gemeinschaft
This archive was generated by a fusion of
Pipermail (Mailman edition) and