Re: [isabelle] &&, force, inputting facts, again

On Sat, 12 Jul 2008, rpollack at wrote:

> Quoting rpollack at
> > Thanks Makarius,
> >
> > >    by
> > >      (insert h[where S="{}"], force,
> > >       insert h[where S ="UNIV::nat set"], force)
> >
> > This seems the clearest to me.
> 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?

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:

* Isar: the goal restriction operator [N] (default N = 1) evaluates a
method expression within a sandbox consisting of the first N
sub-goals, which need to exist.  For example, ``simp_all [3]''
simplifies the first three sub-goals, while (rule foo, simp_all)[]
simplifies all new goals that emerge from applying rule foo to the
originally first one.

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).


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.