Email Gateway (Aug 18 2022 at 12:11): Email Gateway (Aug 18 2022 at 12:11):From: Makarius <makarius@sketis.net>
Proper Isar does not provide fine-grained goal adressing, which is
considered part of the tactical world. The using/apply form is as close
to that as you can get -- in the end it is up to the individual proof
methods to make use of the offered facts in a sensible way, i.e. a method
that operates on a single subgoal (force, blast, fast etc) will only
insert the facts into that goal.
In the "insert" above I actually overlooked that the facts get inserted
into all subgoals. There is relatively recent way to limit the scope of
method expressions to a prefix of the given subgoals, cf. the following
(old) entry in NEWS:
Of course, as the method expressions get more and more complicated the
idea of nicely structured Isar proof texts is getting more and more
diluted. In fact, using just a comma in 'by' method statements is already
leaving the pure world of proof texts. (This is why I would prefer the
double using/apply form over the composition of four methods in the
insert/force form).
Makarius
Email Gateway (Aug 18 2022 at 12:11):From: rpollack@inf.ed.ac.uk
Quoting rpollack@inf.ed.ac.uk:
I was happy too soon. This proof sends both facts to "force" on the
second goal, thus is slow. The other proof you suggested
using h[where S="{}"] apply force
using h[where S ="UNIV::state set"] apply force
done
is fast, and does the intended search, but isn't pure Isar. Does Isar
have a vernacular form that sends the first fact to the first goal, and
only the second fact to the second goal, without restating the second
goal?
Best,
Randy
Last updated: May 03 2024 at 08:18 UTC