[isabelle] Domain proof

Showing 1-3 of 3 messages
 [isabelle] Domain proof Roger H. 1/17/14 8:10 AM Hi, how can i prove lemma "dom (SOME b. dom b = A) = A" Thank you! Re: [isabelle] Domain proof Peter Lammich 1/17/14 8:40 AM 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! > Re: [isabelle] Domain proof Manuel Eberl 1/17/14 9:23 AM 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