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



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.


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.

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

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


Using patterns, we can slightly improve the first presentation

  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)"
	      (is "?snd")
    using h[where S="{}"] proof force
    show "?snd" using h[where S ="UNIV::nat set"] by force
  qed

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!" (Bug?)


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?


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?

Thanks,
Randy

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