Re: [isabelle] includes bundle works only in first case



Hi Makarius,

thanks for the explanation.

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"
using [[show_types]]
proof
next
show "y = y" ..
qed
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.

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
separated.
In my real use case, each goal had the full fix-assume-show chain, so the next was necessary there.

Here is an alternative form that includes a bundle in the context of a toplevel
statement:

lemma
includes test
shows "test xs = []" and "test ys = []"
proof -
show "test xs = []" by simp
next -- "redundant"
show "test ys = []" by simp
qed
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.

Andreas

--
Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Am Fasanengarten 5, Geb. 50.34, Raum 025
76131 Karlsruhe

Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
http://pp.info.uni-karlsruhe.de
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 MHonArc.