*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] &&, force, inputting facts, patterns, naming of lemmas?*From*: Randy Pollack <rpollack at inf.ed.ac.uk>*Date*: Thu, 10 Jul 2008 16:12:46 +0100

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.

**Follow-Ups**:

- Previous by Date: Re: [isabelle] do hardware verification by Isabelle
- Next by Date: [isabelle] &&, force, inputting facts, patterns, naming of lemmas?
- Previous by Thread: [isabelle] RDP'09: Call for Workshop Proposals
- Next by Thread: Re: [isabelle] &&, force, inputting facts, patterns, naming of lemmas?
- 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