*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Domain proof*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Fri, 17 Jan 2014 18:20:10 +0100*In-reply-to*: <1389976441.2717.7.camel@lapbroy33>*References*: <DUB124-W2BC80B14532550F749C8D8FB80@phx.gbl> <1389976441.2717.7.camel@lapbroy33>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.1.0

On my system, the nicest proof sledgehammer finds (after I provide a suitable witness, as Peter suggested) is something like "by (metis (lifting, full_types) dom_const dom_restrict inf_top.left_neutral someI_ex)", which takes over a second to run. These proofs often get a bit tricky because Higher Order Unification does strange things with the someI/someI_ex rules and therefore, one often has to instantiate them manually. I would prove your lemmas like this: lemma "dom (SOME b. dom b = A) = A" by (rule someI_ex[where P = "λb. dom b = A"], rule exI[where x = "(λ_. Some undefined) |` A"], simp) Or, alternatively, if you prefer a more readable Isar proof: lemma "dom (SOME b. dom b = A) = A" proof- let ?f = "(λ_. Some undefined) |` A" have "dom ?f = A" by simp thus ?thesis by (rule someI[where P = "λb. dom b = A"]) qed In case you're wondering what "(λ_. Some undefined) |` A" is: "(λ_. Some undefined)" is simply a partial function that is defined everywhere and always returns "undefined", which is some fixed value of your codomain type about which you know nothing – except that it exists. |` A then restricts this function to A, i.e. returns "None" everywhere except for values in A. You could also write "(λx. if x ∈ A then Some undefined else None)" Note that without the explicit "where" instantiations in someI and someI_ex, it does not work because unification does not produce the unifier I want. In fact, I'm curious as to why this happens myself. Can anybody explain this? Cheers, Manuel On 01/17/2014 05:34 PM, Peter Lammich wrote: > On Fr, 2014-01-17 at 18:03 +0200, Roger H. wrote: >> Hi, >> >> how can i prove >> >> lemma "dom (SOME b. dom b = A) = A" >> > You have to show that there is such a beast b, ie, > > proof - > obtain b where "dom b = A" ... > thus ?thesis > sledgehammer (*Should find a proof now, using the rules for SOME, > probably SomeI*) > > -- Peter > > >> Thank you! >> > >

**References**:**[isabelle] Domain proof***From:*Roger H .

**Re: [isabelle] Domain proof***From:*Peter Lammich

- Previous by Date: Re: [isabelle] Domain proof
- Next by Date: Re: [isabelle] conflicting versions
- Previous by Thread: Re: [isabelle] Domain proof
- Next by Thread: [isabelle] Auto-expand fixed constant in type class
- Cl-isabelle-users January 2014 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