*To*: rpollack at inf.ed.ac.uk*Subject*: Re: [isabelle] &&, force, inputting facts, again*From*: Makarius <makarius at sketis.net>*Date*: Sat, 12 Jul 2008 22:07:01 +0200 (CEST)*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <20080712182835.o1s3a3vy00k008gk@mail.inf.ed.ac.uk>*References*: <20080712182835.o1s3a3vy00k008gk@mail.inf.ed.ac.uk>

On Sat, 12 Jul 2008, rpollack at inf.ed.ac.uk wrote: > Quoting rpollack at inf.ed.ac.uk: > > > 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). Makarius

**References**:**Re: [isabelle] &&, force, inputting facts, again***From:*rpollack

- Previous by Date: Re: [isabelle] &&, force, inputting facts, again
- Next by Date: Re: [isabelle] Help with finite set comprehension proof
- Previous by Thread: Re: [isabelle] &&, force, inputting facts, again
- Next by Thread: [isabelle] About HOL BNF and inner syntax error
- Cl-isabelle-users July 2008 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list