Re: [isabelle] &&, force, inputting facts, patterns, naming of lemmas?



Thanks Makarius,

   by
     (insert h[where S="{}"], force,
      insert h[where S ="UNIV::nat set"], force)

This seems the clearest to me.

Names: I guessed that one can name the two conclusions, "first" and
"second", but I guessed their top-level names would be "lemmaName.first"
and "lemmaName.second", while in fact their top-level names are "first"
and "second".  Any comment Makarius?

[...]

Anyway, you can approximate the desired effect by omitting "first" and
"second" and merely use lemmaName(1) and lemmaName(2) later.

With this kind of theorem with shared assumptions I often want something like:

 note shared = lemmaName[of ..., OF ...]
 ... using shared(1) ...  ... using shared(2) ...

This cannot be done using the names "first" and "second" as Isar treats them now, but could be done if "first" and "second" were qualifiers as I suggested:

 note shared = lemmaName[of ..., OF ...]
 ... using shared.first ...  ... using shared.second ...

This is a minor point, but I think we agree that user-given names should be well supported by Isar.

Best,
Randy
--
Quoting Makarius <makarius at sketis.net>:

On Thu, 10 Jul 2008, Randy Pollack wrote:

Consider the following example (in Isabelle 2008):

  consts
    Req :: "nat => bool"

  lemma lemmaName:
    assumes h:
    "!!(S::nat set) (s::nat).
       (!!z. P' z s ==> (Q' z t & (Ball S Req))) ==>
       (!!z. P z s ==> (Q z t & (Ball S Req)))"
    shows first:"(!!z. P' z s ==> Q' z t) ==> (!!z. P z s ==> Q z t)"
      and second:
        "(ALL s. ((EX  z. P z s) --> (EX z'. P' z' s))) | (ALL u. Req u)"
    using h[where S="{}"] proof force
    show "(ALL s. (EX z. P z s) --> (EX z'. P' z' s)) | (ALL u. Req u)"
      using h[where S ="UNIV::nat set"] by force
  qed

The informal proof is:

  first goal by classical reasoning taking S={} in h,
  second goal by classical reasoning taking S=nat.

My Isar proof is ugly and asymetrical, forcing me to restate the
second conclusion, but not the first conclusion.

How can I express the proof I want in Isar without restating the
second goal?

Here is a more symmetric proof without repeating statements:

   using h[where S="{}"] apply force
   using h[where S ="UNIV::nat set"] apply force
   done

This works because 'using' can be given any number of times in the
refinement part of a proof, and 'apply' resets the current facts
altogether. While this is not fully orthodox "Isar", I would say it is
better than the other variants.


Another Isar proof is:

  using h[where S="{}"] h[where S ="UNIV::nat set"] by (force, force)

This succeeds but is also ugly because we give both facts to both
goals.  This is also very much slower.

Here you can avoid the duplicate use of facts like this:

   by
     (insert h[where S="{}"], force,
      insert h[where S ="UNIV::nat set"], force)

In the form

 using facts by initial_method terminal_method

the constituents of initial_method all see the facts, for "force" they are
inserted into the goal state before emarking on the automated proof
search.

Note that a similar unwanted effect of duplicating irrelevant facts
happens in the popular pattern

 using facts by (cases, auto)   -- BAD

which is spelled out properly like this

 using facts by cases auto

Here only the initial method is exposed to the original list of facts.
As you have noted, this canonical Isar step does not work equally well
with multiple goal statements, though.


In both proofs it seems that the first "force" neither fails nor
finishes the goal, which disagrees with what the HOL tutorial says about
"force".

The tutorial speaks about a single subgoal only, but here you have two of
them.  The first force solves the first one, the second is remaining.


Using patterns, we can slightly improve the first presentation
But syntax

 lemma lemmaName:
   assumes h:
   "!!(S::nat set) (s::nat).
      (!!z. P' z s ==> (Q' z t & (Ball S Req))) ==>
      (!!z. P z s ==> (Q z t & (Ball S Req)))"
   shows first:"(!!z. P' z s ==> Q' z t) ==> (!!z. P z s ==> Q z t)"
                      (is "?fst")
                -- "  ^^^^^^^^^^^ "
   and second:
     "(ALL s. ((EX  z. P z s) --> (EX z'. P' z' s))) | (ALL u. Req u)"
                      (is "?snd")

is rejected: "Pattern match failed!"

This is because the pattern matches only object-logic statements (bool):
the proposition ?fst is actually the term "Trueprop ?fst". To match
against a structured rule statement you need something like (is "PROP
?fst"); using that whole thing later will be a bit cumbersome, though.
In particular, show "PROP ?fst" is a bit flaky, bacause it does not
enforce unification of the premise part, only the conclusion.  In general
sub-structured

 show "!!x. A x ==> B x"

should be replaced by

 fix x
 assume A x
 show B x

This means in the worst case one needs to introduce separate abbreviations
for the premises and the conclusion, abstracted over the parameters.  It
is usually better to try hard writing the statement and proof in a way
that avoids such term references altogether.


Names: I guessed that one can name the two conclusions, "first" and
"second", but I guessed their top-level names would be "lemmaName.first"
and "lemmaName.second", while in fact their top-level names are "first"
and "second".  Any comment Makarius?

Hard to say what is the form with least surprise.  Back then, when
introducing this form of ``long'' statements I did not come up with the
idea of qualified names here.

Anyway, you can approximate the desired effect by omitting "first" and
"second" and merely use lemmaName(1) and lemmaName(2) later.


Finally, the following is also rejected:

  lemma
    assumes h:
    "!!(S::nat set) (s::nat).
       (!!z. P' z s ==> (Q' z t & (Ball S Req))) ==>
       (!!z. P z s ==> (Q z t & (Ball S Req)))"
    shows "(!!z. P' z s ==> Q' z t) ==> (!!z. P z s ==> Q z t)"
    using h[where S="{}"] proof force
    show "(ALL s. (EX z. P z s) --> (EX z'. P' z' s)) | (ALL u. Req u)"
      using h[where S ="UNIV::nat set"] by force

*** empty result sequence -- proof command failed
*** At command "proof".

I only removed the second goal from the statement of the lemma, and
tried to use the proof of the first goal that worked before.  Bug?

As usual: whenever something fails to work but really should work, it is
due to unexpectedly general typing.  With less text in the statement, the
inferred types can come out more general; and indeed the arguments of Q
now get types of Pure's topsort {}, not HOL's "type" class.


	Makarius




--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.






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