*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] &&, force, inputting facts, patterns, naming of lemmas?*From*: rpollack at inf.ed.ac.uk*Date*: Sat, 12 Jul 2008 14:55:14 +0100*Cc*: isabelle-users at cl.cam.ac.uk*User-agent*: Internet Messaging Program (IMP) H3 (4.0.4)

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

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

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.

- Previous by Date: Re: [isabelle] Help with finite set comprehension proof
- Next by Date: Re: [isabelle] &&, force, inputting facts, again
- Previous by Thread: Re: [isabelle] Help with finite set comprehension proof
- Next by Thread: Re: [isabelle] &&, force, inputting facts, again
- 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